proposition: Lemma iso_rec_dir_complexe : forall (a b c : C) (A B C : PO), a = affixe A -> b = affixe B -> c = affixe C -> isocele_rectangle_direct A B C -> Cplus c (Copp a) = Cmult i (Cplus b (Copp a)).
proof: Proof. unfold isocele_rectangle_direct, isocele in |- *; intros. elim H2; [ intros H3 H4; elim H4; [ intros H5 H6; try clear H4 H2; try exact H6 ] ]. rewrite forme_polaire_i. apply rotation_complexe with (J := A) (M := B) (M' := C); auto. apply rotation_def2; auto. Qed.