proposition: Lemma deux_iso_rec_dir_complexe : forall (a b c d e : C) (A B C D E : PO), a = affixe A -> b = affixe B -> c = affixe C -> d = affixe D -> e = affixe E -> isocele_rectangle_direct A B C -> isocele_rectangle_direct A D E -> Cplus e (Copp c) = Cmult i (Cplus d (Copp b)).
proof: Proof. intros a b c d e A B C D E aA bB cC dD eE ABC ADE. generalize (iso_rec_dir_complexe aA bB cC ABC); intros H11. generalize (iso_rec_dir_complexe aA dD eE ADE); intros H12. replace (Cplus e (Copp c)) with (Cplus (Cplus e (Copp a)) (Copp (Cplus c (Copp a)))); [ idtac | ring ]. rewrite H12; auto. rewrite H11; auto. replace (Cplus d (Copp b)) with (Cplus (Cplus d (Copp a)) (Copp (Cplus b (Copp a)))); ring. Qed.