@options;

@figure;
  B = point( -7.77 , 5.52 );
  E = point( 4.02 , 3.1 );
  F = point( 5.4 , -2.26 );
  sBF = segment( B , F );
  A = pointsur( sBF , 0.62 );
  dAE = droite( A , E )  { i };
  sEF = segment( E , F );
  dBC = parallele( B , sEF )  { i };
  C = intersection( dBC , dAE );
  sAB = segment( A , B );
  sAC = segment( A , C );
  sBC = segment( B , C );
  sAE = segment( A , E );
  J = symetrique( E , A );
  I = symetrique( F , A );
  sIJ = segment( I , J );

RP1
RESUME
La double égalité est l'expression principale. Les égalités suivantes servent à remplacer certains élèments de l'expression principale.
SI
egal3 X Y Z
egal m n
egal p q
egal r s
ALORS
egal3 U V W

MODE
bao
sans_permutation
SI
milieu A F I
milieu A E J
appartient_segment I A B
appartient_segment J A C
parallelogramme E I J F
para (EF) (IJ)
para (IJ) (BC)
egal EF IJ
ALORS
egal3 qo(AI;AB) qo(AJ;AC) qo(IJ;BC)
egal3 qo(AE;AC) qo(AF;AB) qo(EF;BC)

T1 triangle
RESUME
Dans un triangle, une droite qui passe par les milieux de deux côtés est parallèle au troisième côté.
CONTEXTE
Dans le triangle {M}{N}{P} |  Dans un triangle,
SI
milieu Q M N | le milieu d'un côté
milieu R M P | le milieu d'un autre côté
ALORS
para (QR) (PN) | la droite qui passe par ces milieux est parallèle au troisième côté.
--
T2 triangle
RESUME
Dans un triangle, si une droite passe par le milieu d'un côté et est parallèle à un deuxième côté, alors cette droite passe par le milieu du troisième côté.
CONTEXTE
Dans le triangle {M}{N}{P} | Dans un triangle
SI
inter Q d (MN) | une droite coupe un côté du triangle
milieu Q M N | en un point qui est le milieu de ce côté
para d (PN) | cette droite est parallèle au deuxième côté
inter R d (PM) | cette droite coupe le troisième côté en un certain point
ALORS
milieu R M P | ce point est le milieu du troisième côté.
--
T2bis triangle
EVIDENCE
EV1 EV2
RESUME
Dans un triangle, si une droite passe par le milieu d'un côté et est parallèle à un deuxième côté, alors cette droite passe par le milieu du troisième côté.
CONTEXTE
Dans le triangle {M}{N}{P} | Dans un triangle,
SI
passemilieu d M N | une droite qui passe par le milieu d'un côté
para d (PN) | et qui est parallèle à un deuxième côté
ALORS
passemilieu d M P | cette droite passe par le milieu du troisième côté.
--
T2ter triangle
RESUME
Dans un triangle, si une droite passe par le milieu d'un côté et est parallèle à un deuxième côté, alors cette droite passe par le milieu du troisième côté.
CONTEXTE
Dans le triangle {M}{N}{P} | Dans un triangle,
SI
para (QR) (PN) | une droite parallèle à un côté
milieu Q M N | qui passe par le milieu d'un deuxième côté.
inter S (QR) (PM) | cette droite coupe le troisième côté en un certain point
ALORS
milieu S M P | ce point est le milieu du troisième côté.
--
P1 parallélogramme
RESUME
Dans un parallélogramme, les diagonales se coupent en leur milieu.
SI
parallelogramme M N P Q | un parallélogramme,
inter O (MP) (NQ) | ses diagonales sont sécantes en un point
ALORS
milieu O M P | ce point est le milieu d'une diagonale
milieu O N Q | ce point est le milieu de l'autre diagonale.
--
P1r parallélogramme
RESUME
Un quadrilatère dont les diagonales se coupent en leur milieu est un parallèlogramme.
CONTEXTE
Dans le quadrilatère {M}{N}{P}{Q} | Dans un quadrilatère,
SI
milieu O M P | un point milieu d'une diagonale
milieu O N Q | ce même point milieu d'une autre diagonale
ALORS
parallelogramme M N P Q | c'est un parallélogramme,
--
P2 parallélogramme
RESUME
Dans un parallélogramme, les côtés opposés sont parallèles.
SI
parallelogramme M N P Q | un parallélogramme,
ALORS
para (MN) (PQ)| deux côtés opposés sont parallèles
para (NP) (MQ) | les deux autres côtés opposés sont parallèles
--
P2r parallélogramme
RESUME
Un quadrilatère dont les côtés opposés sont parallèles est un parallélogramme.
CONTEXTE
Dans le quadrilatère {M}{N}{P}{Q}| Dans un quadrilatère
SI
para (MN) (PQ)| deux côtés opposés parallèles
para (NP) (MQ) | les deux autres côtés opposés parallèles
ALORS
parallelogramme M N P Q | c'est un parallélogramme,
--
P3 parallélogramme
RESUME
Dans un parallélogramme, les côtés opposés sont de même longueur.
SI
parallelogramme M N P Q | un parallélogramme,
ALORS
egal MN PQ | deux côtés opposés sont de même longueur
egal NP MQ | les deux autres côtés opposés sont de même longueur
--
P3r parallélogramme
RESUME
Un quadrilatère non croisé dont les côtés opposés sont de même longueur est un parallélogramme.
CONTEXTE
Dans le quadrilatère non croisé {M}{N}{P}{Q}| Dans un quadrilatère non croisé
SI
egal MN PQ | deux côtés opposés de même longueur
egal NP MQ | les deux autres côtés opposés de même longueur
ALORS
parallelogramme M N P Q | c'est un parallélogramme,
--
D1 droite
RESUME
Si deux droites sont parallèles, toute droite perpendiculaire à l'une est perpendiculaire à l'autre
SI
para d1 d2 | deux droites parallèles
perp d3 d1 | une droite perpendiculaire à l'une
ALORS
perp d3 d2 | cette droite est perpendiculaire à l'autre.
--
D2 droite
RESUME
Si deux droites sont perpendiculaires, toute droite perpendiculaire à l'une est parallèle à l'autre
SI
perp d1 d2 | deux droites perpendiculaires
perp d3 d1 | une droite perpendiculaire à l'une
ALORS
para d3 d2 | cette droite est parallèle à l'autre.
--
D3 droite
RESUME
Si deux droites sont parallèles, toute droite parallèle à l'une est parallèle à l'autre
SI
para d1 d2 | deux droites parallèles,
para d3 d1 | une droite parallèle à l'une
ALORS
para d3 d2 | cette droite est parallèle à l'autre.
--
S1 symétrie
RESUME
Dans une symétrie centrale, le centre de symétrie est le milieu du segment dont les extrémités sont un point et son image.
SI
sym_centrale N M O
ALORS
milieu O M N
--
TH1 Thalès
RESUME
théorème de Thalès à l'intérieur d'un triangle
CONTEXTE
Dans le triangle {O}{M}{N} | Dans un triangle
SI
appartient_segment Q O M | un point appartient à un côté
appartient_segment R O N | un autre point appartient à un autre côté
para (QR) (MN) | la droite constituée par ses deux points est parallèle au troisième côté.
ALORS
egal3 qo(OQ;OM) qo(OR;ON) qo(QR;MN) | une double égalité de rapports de longueur.
--
M1 milieu
RESUME
Le milieu partage le segment en deux parties de même longueur
SI
milieu O M N
ALORS
egal OM ON