proposition: Lemma ROND_RON : forall O I J : PO, repere_orthonormal_direct O I J -> repere_orthonormal O I J.
proof: Proof. unfold repere_orthonormal_direct, repere_orthonormal in |- *; intros. elim H; intros H0 H1; try clear H; try exact H1. split; [ auto with geo | try assumption ]. Qed.