proposition: Theorem deux_isocele_rectangle_direct : forall A B C D E : PO, B <> D :>PO -> isocele_rectangle_direct A B C -> isocele_rectangle_direct A D E -> distance B D = distance C E /\ cons_AV (vec B D) (vec C E) = image_angle pisurdeux.
proof: Proof. intros. elim existence_affixe_point with (M := A); intros a; intros. elim existence_affixe_point with (M := B); intros b; intros. elim existence_affixe_point with (M := C); intros c; intros. elim existence_affixe_point with (M := D); intros d; intros. elim existence_affixe_point with (M := E); intros e; intros. cut (Cplus e (Copp c) = Cmult i (Cplus d (Copp b))); intros. cut (distance B D = distance C E); intros. cut (C <> E); intros. split; [ try assumption | idtac ]. cut (Cplus d (Copp b) <> zeroC); intros. cut (Cplus e (Copp c) <> zeroC); intros. rewrite (angle_vecteurs_arguments (A:=B) (B:=D) (A':=C) (B':=E) (z:=Cplus d (Copp b)) (z':=Cplus e (Copp c))); auto with geo. rewrite H7; rewrite forme_polaire_i; rewrite Cmult_argument; auto. rewrite argument_module_un. elim existence_argument with (z := Cplus d (Copp b)); [ intros; try clear existence_argument | auto ]. rewrite H12; repeat rewrite <- mes_opp. repeat rewrite <- add_mes_compatible. replace (pisurdeux + x + - x) with pisurdeux; [ auto | ring ]. auto with geo. apply diff_nonzero with (3 := H9); auto. apply diff_nonzero with (3 := H); auto. apply isometrie_distinct with (2 := H8); auto. rewrite <- (module_difference H3 H5). rewrite <- (module_difference H4 H6). rewrite H7; rewrite forme_polaire_i; rewrite Cmult_module; rewrite complexe_polaire_module; ring. apply (@deux_iso_rec_dir_complexe a b c d e A B C D E); auto. Qed.