proposition: Lemma produit_distance_distinct : forall (A B C D : PO) (k : R), k <> 0 -> A <> B -> distance C D = k * distance A B -> C <> D.
proof: Proof. intros. contrapose H0. assert (distance A B = 0); auto with geo. replace (distance A B) with (/ k * distance C D). rewrite H2. replace (distance D D) with 0. ring. symmetry in |- *; auto with geo. rewrite H1. field; auto. Qed.