proposition: Lemma argument_difference : forall (a b : C) (A B : PO), A <> B -> a = affixe A -> b = affixe B -> argument (Cplus b (Copp a)) = cons_AV (vec O I) (vec A B).
proof: Proof. intros. cut (Cplus b (Copp a) = affixe_vec (vec A B)); intros. elim existence_representant_vecteur with (A := O) (B := A) (C := B); intros D; intros. cut (Cplus b (Copp a) = affixe D); intros. rewrite (argument_def (M:=D) (z:=Cplus b (Copp a))); auto with geo. rewrite H3; auto. red in |- *; intros; apply H. apply vecteur_nul_conf. rewrite <- H3; rewrite <- H5; Ringvec. cut (Cplus b (Copp a) = affixe_vec (vec O D)); intros; auto with geo. rewrite H2; rewrite H3; auto with geo. apply affixe_vec_AB; auto. Qed.