proposition: Lemma argument_quotient : forall (a b d e : C) (A B D E : PO), A <> B :>PO -> D <> E :>PO -> a = affixe A -> b = affixe B -> d = affixe D -> e = affixe E -> argument (Cdiv (Cplus b (Copp a)) (Cplus e (Copp d))) = cons_AV (vec D E) (vec A B).
proof: Proof. intros. cut (Cplus b (Copp a) <> zeroC); intros. cut (Cplus e (Copp d) <> zeroC); intros. rewrite Cdiv_def; auto with geo. rewrite Cmult_argument; auto with geo. rewrite Cinv_argument; auto with geo. rewrite (argument_difference (a:=a) (b:=b) (A:=A) (B:=B)); auto with geo. rewrite (argument_difference (a:=d) (b:=e) (A:=D) (B:=E)); auto with geo. apply diff_nonzero with (3 := H0); auto. apply diff_nonzero with (3 := H); auto. Qed.