EV1 évidence
SI
egal X qo(M;2)
egal Y qo(N;2)
egal M N
ALORS
egal X Y
--
EV2 évidence
SI
egal X qo(M;2)
egal Y qo(N;2)
egal M N
ALORS
egal X Y
--
EV3 évidence
SI
para (MN) (PQ)
milieu X M N
milieu Y P Q
ALORS
para (XM) (YP)
--
EV4 évidence
SI
para (MN) (PQ)
milieu X M N
milieu Y P Q
ALORS
para (XM) (YP)

MODE
bao
SI
losange A B C D
milieu I A B
milieu J B C
milieu K C D
milieu L A D
parallelogramme I J K L
ALORS
rectangle I J K L

T1 triangle milieu
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é.
--
T1b triangle milieu
RESUME
Dans un triangle, un segment qui joint les milieux de deux côtés mesure la moitié du 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
egal QR qo(PN;2) | le segment qui joint ces milieux mesure la moitié du troisième côté
--
T2 triangle milieu
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é.
--
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,
--
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,
--
RL1 rectangle_losange
RESUME
Un parallélogramme dont 2 côtés consécutifs sont perpendiculaires est un rectangle
SI
parallelogramme M N P Q | un parallélogramme
perp (MN) (NP) | deux côtés consécutifs perpendiculaires
ALORS
rectangle M N P Q | c'est un rectangle
--
RL1r rectangle_losange
RESUME
Deux côtés consécutifs d'un rectangle sont perpendiculaires
SI
rectangle M N P Q
ALORS
perp (MN) (NP)
perp (NP) (PQ)
perp (PQ) (QM)
perp (QM) (MN)
--
RL2 rectangle_losange
RESUME
Un parallélogramme dont les diagonales sont de même longueur est un rectangle
SI
parallelogramme M N P Q | un parallélogramme
egal MP NQ | ses diagonales sont de même longueur
ALORS
rectangle M N P Q | c'est un rectangle
--
RL2r rectangle_losange
RESUME
Les diagonales d'un rectangle sont de même longueur. 
SI
rectangle M N P Q | un rectangle
ALORS
egal MP NQ | ses diagonales sont de même longueur
--
RL3 rectangle_losange
RESUME
Un parallélogramme dont 2 côtés consécutifs sont de même longueur est un losange
SI
parallelogramme M N P Q | un parallélogramme
egal MN NP | deux côtés consécutifs de même longueur
ALORS
losange M N P Q | c'est un losange
--
RL3r rectangle_losange
RESUME
Deux côtés consécutifs d'un losange sont de même longueur
SI
losange M N P Q
ALORS
egal MN NP
egal NP PQ
egal PQ QM
egal QM MN
--
RL4 rectangle_losange
RESUME
Un parallélogramme dont les diagonales sont perpendiculaires est un losange
SI
parallelogramme M N P Q | un parallélogramme
perp (MP) (NQ) | ses diagonales sont perpendiculaires
ALORS
losange M N P Q | c'est un losange
--
RL4r rectangle_losange
RESUME
Les diagonales d'un losange sont perpendiculaires 
SI
losange M N P Q | un losange
ALORS
perp (MP) (NQ) | ses diagonales sont perpendiculaires
--
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.
--
M1 milieu
RESUME
Le milieu partage le segment en deux parties de même longueur
SI
milieu O M N
ALORS
egal OM ON
--
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