proposition: Lemma complexe_iso_rec_dir : forall (a b c : C) (A B C : PO), a = affixe A -> b = affixe B -> c = affixe C -> A <> B -> Cplus c (Copp a) = Cmult i (Cplus b (Copp a)) -> isocele_rectangle_direct A B C.
proof: Proof. unfold isocele_rectangle_direct, isocele in |- *; intros. cut (distance A B = distance A C); intros. cut (A <> C); intros. split; [ try assumption | idtac ]. split; [ try assumption | idtac ]. cut (Cplus b (Copp a) <> zeroC); intros. cut (Cplus c (Copp a) <> zeroC); intros. rewrite (angle_vecteurs_arguments (A:=A) (B:=B) (A':=A) (B':=C) (z:=Cplus b (Copp a)) (z':=Cplus c (Copp a))); auto with geo. rewrite H3; rewrite forme_polaire_i; rewrite Cmult_argument; auto. rewrite argument_module_un. elim existence_argument with (z := Cplus b (Copp a)); [ intros; try clear existence_argument | auto ]. rewrite H8; 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 := H5); auto. apply diff_nonzero with (3 := H2); auto. apply isometrie_distinct with (2 := H4); auto. rewrite <- (module_difference H H0). rewrite <- (module_difference H H1). rewrite H3; rewrite forme_polaire_i; rewrite Cmult_module; rewrite complexe_polaire_module; ring. Qed.