proposition: Lemma triangles_isometriques_indirects : forall (A B C A' B' C' : PO) (x x' y y' : R), A <> B :>PO -> A <> C :>PO -> B <> C :>PO -> distance A' B' = distance A B -> distance A' C' = distance A C -> cons_AV (vec A B) (vec A C) = cons_AV (vec A' C') (vec A' B') :>AV -> image_angle x = cons_AV (vec B C) (vec B A) :>AV -> image_angle x' = cons_AV (vec B' C') (vec B' A') :>AV -> image_angle y = cons_AV (vec C A) (vec C B) :>AV -> image_angle y' = cons_AV (vec C' A') (vec C' B') :>AV -> distance B' C' = distance B C /\ cos x = cos x' /\ cos y = cos y'.
proof: Proof. intros. mesure A B A C. cut (A' <> B' /\ A' <> C'); intros. elim H10; intros H22 H23; try clear H10. cut (distance B' C' = distance B C); intros. cut (B' <> C'). intros H21. cut (2 <> 0). intros H24. split; [ try assumption | idtac ]. split; [ try assumption | idtac ]. cut (Rsqr (distance C A) = Rsqr (distance B C) + Rsqr (distance B A) + - (2 * (distance B C * (distance B A * cos x)))); intros. cut (Rsqr (distance C' A') = Rsqr (distance B' C') + Rsqr (distance B' A') + - (2 * (distance B' C' * (distance B' A' * cos x')))); intros. cut (2 * (distance B C * distance B A) * cos x = 2 * (distance B' C' * distance B' A') * cos x'); intros. apply resolution2 with (x := 2 * (distance B C * distance B A)) (y := 2 * (distance B' C' * distance B' A')); auto with geo real. rewrite (distance_sym B' A'); rewrite H10; rewrite H2; rewrite (distance_sym B A); ring. replace (2 * (distance B' C' * distance B' A') * cos x') with (Rsqr (distance B' C') + Rsqr (distance B' A') + - Rsqr (distance C' A')). replace (2 * (distance B C * distance B A) * cos x) with (Rsqr (distance B C) + Rsqr (distance B A) + - Rsqr (distance C A)). rewrite (distance_sym B' A'); rewrite (distance_sym C' A'); rewrite H10; rewrite H2; rewrite H3; rewrite (distance_sym B A); rewrite (distance_sym C A); ring. rewrite H11; ring. rewrite H12; ring. apply Al_Kashi; auto. apply Al_Kashi; auto. cut (Rsqr (distance A B) = Rsqr (distance C A) + Rsqr (distance C B) + - (2 * (distance C A * (distance C B * cos y)))); intros. cut (Rsqr (distance A' B') = Rsqr (distance C' A') + Rsqr (distance C' B') + - (2 * (distance C' A' * (distance C' B' * cos y')))); intros. cut (2 * (distance C A * distance C B) * cos y = 2 * (distance C' A' * distance C' B') * cos y'); intros. apply resolution2 with (x := 2 * (distance C A * distance C B)) (y := 2 * (distance C' A' * distance C' B')); auto with geo real. rewrite (distance_sym C' A'); rewrite H3; rewrite (distance_sym C' B'); rewrite H10; rewrite (distance_sym C B); rewrite (distance_sym C A); ring. replace (2 * (distance C A * distance C B) * cos y) with (Rsqr (distance C A) + Rsqr (distance C B) + - Rsqr (distance A B)). replace (2 * (distance C' A' * distance C' B') * cos y') with (Rsqr (distance C' A') + Rsqr (distance C' B') + - Rsqr (distance A' B')). rewrite (distance_sym C' B'); rewrite (distance_sym C' A'); rewrite H10; rewrite H2; rewrite H3; rewrite (distance_sym C B); rewrite (distance_sym C A); ring. rewrite H12; ring. rewrite H11; ring. apply Al_Kashi; auto. apply Al_Kashi; auto. discrR. apply dist_non_nulle; rewrite H10; auto with geo. apply distance_carre. mesure A B A C. rewrite (Al_Kashi (A:=A) (B:=B) (C:=C) (a:=x1)); auto. rewrite (Al_Kashi (A:=A') (B:=B') (C:=C') (a:=- x1)); auto. rewrite H2; rewrite H3; rewrite cos_paire; ring. apply (mes_oppx (A:=A') (B:=C') (C:=A') (D:=B') (x:=x1)); auto. rewrite H10; 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.