proposition: Lemma isocele_angles_base : forall A B C : PO, A <> B -> A <> C -> B <> C -> isocele A B C -> cons_AV (vec B C) (vec B A) = cons_AV (vec C A) (vec C B).
proof: Proof. intros A B C H H0 H1; try assumption. soit_milieu B C K. elim (classic (A = K)); intros. apply permute_angles; auto. rewrite <- H6 in H5. rewrite <- H6 in H2. rewrite <- (angles_milieu (A:=C) (B:=B) (C:=C) (I:=A)); auto. rewrite <- (angles_milieu2 (A:=B) (B:=B) (C:=C) (I:=A)); auto with geo. cut (orthogonal (vec B C) (vec K A)); intros. cut (cons_AV (vec K B) (vec K A) = cons_AV (vec K A) (vec K C)); intros. cut (cons_AV (vec A B) (vec A K) = cons_AV (vec A K) (vec A C)); intros. rewrite (angles_milieu (A:=A) (B:=B) (C:=C) (I:=K)); auto. generalize (somme_triangle (A:=A) (B:=B) (C:=K)); auto; intros. generalize (somme_triangle (A:=A) (B:=K) (C:=C)); auto; intros. rewrite (angles_milieu2 (A:=A) (B:=B) (C:=C) (I:=K)); auto. replace (cons_AV (vec B K) (vec B A)) with (plus (image_angle pi) (opp (plus (cons_AV (vec A B) (vec A K)) (cons_AV (vec K A) (vec K B))))). replace (cons_AV (vec C A) (vec C K)) with (plus (image_angle pi) (opp (plus (cons_AV (vec A K) (vec A C)) (cons_AV (vec K C) (vec K A))))). rewrite H9. replace (cons_AV (vec K C) (vec K A)) with (cons_AV (vec K A) (vec K B)); auto with geo. rewrite <- H11; auto. mesure A K A C. mesure K C K A. mesure C A C K. replace (x + (x0 + x1) + - (x + x0)) with x1; auto. ring. rewrite <- H10; auto. mesure K A K B. mesure A B A K. mesure B K B A. replace (x0 + (x1 + x) + - (x0 + x)) with x1; auto. ring. generalize (isocele_mediane_bissectrice (A:=A) (B:=B) (C:=C) (I:=K)); auto; intros. generalize (milieu_angles_orthogonaux (A:=B) (B:=C) (M:=K) (N:=A)); auto; intros. generalize (mediane_isocele_hauteur (A:=A) (B:=B) (C:=C) (I:=K)); auto with geo; intros. Qed.