proposition: Lemma distance_carre : forall A B C D : PO, Rsqr (distance A B) = Rsqr (distance C D) -> distance A B = distance C D.
proof: Proof. unfold Rsqr in |- *; intros. apply carre_egalite_distance; auto with geo. Qed.