proposition: Lemma existence_ROND_AB : forall A B : PO, distance A B = 1 -> exists C : PO, repere_orthonormal_direct A B C.
proof: Proof. intros. elim existence_representant_angle with (A := A) (B := B) (C := A) (x := pisurdeux); [ intros C H0; elim H0; intros H1 H2; try clear H0; try exact H2 | auto ]. exists C; unfold repere_orthonormal_direct in |- *. split; [ try assumption | idtac ]. split; auto with geo. Qed.