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