proposition: Lemma affixe_vec_AB : forall (a b : C) (A B : PO), a = affixe A -> b = affixe B -> Cplus b (Copp a) = affixe_vec (vec A B).
proof: Proof. intros. elim existence_parties_relles_imaginaires with (z := a); intros a1 H2; elim H2; intros a2 H3; try clear H2; try exact H3. elim existence_parties_relles_imaginaires with (z := b); intros b1 H4; elim H4; intros b2 H5; try clear H4; try exact H5. elim cartvec_AB with (a1 := a1) (a2 := a2) (b1 := b1) (b2 := b2) (O := O) (I := I) (J := J) (A := A) (B := B); [ intros H1 H2; try clear cartvec_AB; try exact H2 | eauto with geo | eauto with geo | eauto with geo | eauto with geo | eauto with geo ]. rewrite H5; rewrite H3; rewrite Copp_algebrique; rewrite Cplus_algebrique. rewrite (absvec_ordvec_affixe (a:=b1 + - a1) (b:=b2 + - a2) (A:=A) (B:=B)); auto. Qed.