@options;

@figure;
  A = point( 0.41 , 2.69 );
  B = point( -3.95 , 0.06 );
  sAB = segment( A , B );
  dAC = perpendiculaire( A , sAB )  { i };
  C = pointsur( dAC , 3.02 );
  sBC = segment( B , C );
  sAC = segment( A , C );
  r1 = rotation( C , 90 );
  r2 = rotation( B , -90 );
  r3 = rotation( B , 90 );
  r4 = rotation( A , 90 );
  r5 = rotation( A , -90 );
  r6 = rotation( C , -90 );
  D = image( r2 , C );
  E = image( r1 , B );
  F = image( r3 , A );
  G = image( r5 , B );
  H = image( r4 , C );
  I = image( r6 , A );
  sBF = segment( B , F );
  sFG = segment( F , G );
  sAG = segment( A , G );
  sAH = segment( A , H );
  sHI = segment( H , I );
  sCI = segment( C , I );
  sBD = segment( B , D );  
  sCE = segment( C , E );
  sDE = segment( D , E );
  
  sAD = segment( A , D );
  sAE = segment( A , E );  
  sCF = segment( C , F );  
  sBI = segment( B , I );  

  dAK = perpendiculaire( A , sBC );
  K = intersection( dAK , sDE );
  L = intersection( dAK , sBC );
  sAK = segment( A , K );

EV1
SI
quadrilatere_nc  M N P Q
appartient_segment R M N
appartient_segment S P Q
ALORS
egal ai(MNPQ) so(ai(MRSQ);ai(RNPS))

MODE
bao
SI
carre A B F G
carre B C E D
carre C A H I
appartient_segment L C B
appartient_segment K E D
egal ai(BAD) ai(BCF)
egal ai(CAE) ai(CBI)
egal ai(ABFG) pr(2;ai(BCF))
egal ai(ACIH) pr(2;ai(CBI))
egal ai(BLKD) pr(2;ai(BAD))
egal ai(CLKE) pr(2;ai(CAE))
ALORS
egal ca(BC) so(ca(AB);ca(AC))

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é.
egal QR qo(PN;2) 
--
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é.
--
TI1 triangle_isométrique
RESUME
Caractérisation de deux triangles isométriques.
CONTEXTE
Soient le triangle {M}{N}{P} et le triangle {R}{S}{T} | Soient deux triangles
SI
egal MN RS | un côté de l'un a la même longueur qu'un côté de l'autre
egal MP RT | un deuxième côté de l'un a la même longueur qu'un deuxième côté de l'autre
egal an(NMP) an(SRT) | ces deux côtés forment un angle de même mesure dans chaque triangle
ALORS
tri_iso M N P S R T | ces deux triangles sont isométriques.
--
TI2 triangle_isométrique
Des triangles isométriques ont même aire.
SI
tri_iso M N P S R T
ALORS
egal ai(MNP) ai(SRT)
--
TR1 triangle_rectangle
RESUME
CONTEXTE
SI
tri_rect M N P
ALORS
perp (MN) (MP)
--
EV1 évidence
RESUME
SI
passemilieu d M N
inter P d (MN)
ALORS
milieu P M N
--
EV2 évidence
RESUME
SI
inter P d (MN)
milieu P M N
ALORS
passemilieu d M N
--
EV3 évidence
RESUME
CONTEXTE
{M}, {N}, et {P} sont distincts.
SI
aligne_ordre M N P
ALORS
appartient M (NP)
appartient_segment N M P
appartient P (NM)
--
EV4 évidence
RESUME
CONTEXTE
{M}, {N}, et {P} sont distincts.
SI
aligne M N P
ALORS
appartient M (NP)
appartient N (MP)
appartient P (NM)
--
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,
--
P4 parallélogramme
RESUME
CONTEXTE
SI
parallelogramme M N P Q
appartient R (PQ)
ALORS
egal ai(MNPQ) pr(2;ai(MNR))
--
P5 parallélogramme
RESUME
Un quadrilatère non croisé dont 2 côtés opposés sont parallèles et 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
para (MN) (PQ) | et parallèles
ALORS
parallelogramme M N P Q | c'est un parallélogramme,
--
L1 losagne
RESUME
Un losange a ses côtés de même longueur.
SI
losange M N P Q
ALORS
egal MN NP
egal NP PQ
egal PQ QM
egal QM MN
--
R1 rectangle
RESUME
Un rectangle a 4 angles droits.
SI
rectangle M N P Q
ALORS
perp (MQ) (MN)
perp (NM) (NP)
perp (PN) (PQ)
perp (QP) (QM)
--
R1bis rectangle
RESUME
Un rectangle a 4 angles qui mesurent 90°.
SI
rectangle M N P Q
ALORS
egal an(QMN) 90
egal an(MNP) 90
egal an(NPQ) 90
egal an(PQM) 90
--
R2 rectangle
RESUME
Un quadrilatère qui a 3 angles droits est un rectangle.
SI
perp (MQ) (MN)
perp (NM) (NP)
perp (PN) (PQ)
ALORS
rectangle M N P Q
--
A1 angle
SI
angle_adj O M N P
ALORS
egal an(MOP) so(an(MON);an(NOP))
--
A2 angle
RESUME
Un angle droit mesure 90°.
SI
perp (OM) (ON)
ALORS
egal an(MON) 90
--
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.
--
D4 droite
RESUME
CONTEXTE
Soient {O},{M},{N} et {P} des points distincts
SI
perp (OM) (OP)
perp (ON) (OP)
ALORS
aligne O M N
--
M1 milieu
RESUME
Le milieu partage le segment en deux parties de même longueur
SI
milieu O M N
ALORS
egal OM ON
--
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
CONTEXTE
Dans le triangle {O}{M}{N}
SI
appartient Q (OM)
appartient R (ON)
para (QR) (MN)
ALORS
egal3 qo(OQ;OM) qo(OR;ON) qo(QR;MN) 
--
TH1bis Thalès
RESUME
théorème de Thalès à l'intérieur d'un triangle
CONTEXTE
Dans le triangle {O}{M}{N}
SI
appartient_segment Q O M
appartient_segment R O N
para (QR) (MN)
ALORS
egal3 qo(OQ;OM) qo(OR;ON) qo(QR;MN)
--
RP1 calcul_remplacement
RESUME
Remplace dans une double égalité. La première é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 r s
egal p q
ALORS
egal3 U V W
--
RP2 calcul_remplacement
RESUME
La première égalité est l'expression principale. Les égalités suivantes servent à remplacer certains élèments de l'expression principale.
SI
egal X Y
egal m n
egal p q
egal r s
ALORS
egal U V
--
CA1 calcul_remplacement
RESUME
Deux quantités égales à une même troisième sont égales entre elles.
SI
egal X Y
egal Z Y
ALORS
egal X Z
--
CR1 carré
RESUME
aire d'un carré
SI
carre M N P Q
ALORS
egal ai(MNPQ) ca(MN)