proposition: Lemma cas_egalite_triangle_indirect : forall A B C A' B' C' : PO, A <> B :>PO -> A <> C :>PO -> B <> C :>PO -> distance A' B' = distance A B :>R -> distance A' C' = distance A C :>R -> cons_AV (vec A B) (vec A C) = cons_AV (vec A' C') (vec A' B') :>AV -> distance B' C' = distance B C :>R /\ cons_AV (vec B C) (vec B A) = cons_AV (vec B' A') (vec B' C') :>AV /\ cons_AV (vec C A) (vec C B) = cons_AV (vec C' A') (vec C' B') :>AV.
proof: Proof. intros. cut (A' <> B' /\ A' <> C'); intros. elim H5; intros H6 H7; try clear H5; try exact H7. mesure A B A C. cut (distance B' C' = distance B C). intros H20. cut (B' <> C'). intros H21. mesure B C B A. mesure B' C' B' A'. mesure C A C B. mesure C' A' C' B'. rewrite H8; rewrite H10; rewrite H11. elim triangles_isometriques_indirects with (A := A) (B := B) (C := C) (A' := A') (B' := B') (C' := C') (x := x0) (x' := x1) (y := x2) (y' := x3); [ intros; try exact H0 | auto | auto | auto | auto | auto | auto | auto | auto | auto | auto ]. split; [ try assumption | idtac ]. elim H13; intros H14 H15; try clear H13; try exact H15. apply angles_egaux_triangle_indirect with (x := x0) (x' := x1) (y := x2) (y' := x3); auto. apply dist_non_nulle; rewrite H20; auto with geo. apply distance_carre. rewrite (Al_Kashi (A:=A) (B:=B) (C:=C) (a:=x)); auto. rewrite (Al_Kashi (A:=A') (B:=B') (C:=C') (a:=- x)); auto. rewrite H2; rewrite H3; rewrite cos_paire; ring. apply (mes_oppx (A:=A') (B:=C') (C:=A') (D:=B') (x:=x)); auto. rewrite H5; rewrite H4; auto. split; [ idtac | try assumption ]. apply dist_non_nulle; rewrite H2; auto with geo. apply dist_non_nulle; rewrite H3; auto with geo. Qed.