proposition: Lemma module_quotient : forall (a b d e : C) (A B D E : PO), D <> E :>PO -> a = affixe A -> b = affixe B -> d = affixe D -> e = affixe E -> module (Cdiv (Cplus b (Copp a)) (Cplus e (Copp d))) = distance A B * / distance D E.
proof: Proof. intros. rewrite Cdiv_def. rewrite Cmult_module; rewrite Cinv_module; auto with geo. rewrite (module_difference (a:=a) (b:=b) (A:=A) (B:=B)); auto with geo. rewrite (module_difference (a:=d) (b:=e) (A:=D) (B:=E)); auto with geo. apply diff_nonzero with (3 := H); auto. apply diff_nonzero with (3 := H); auto. Qed.