proposition: Lemma orthonormal_orthogonal : forall O I J : PO, repere_orthonormal O I J -> repere_orthogonal O I J.
proof: Proof. unfold repere_orthonormal in |- *; intros. elim H; intros H0 H1; elim H1; intros H2 H3; try clear H1 H; try exact H3. apply triangle_rectangle_repere; auto with geo. Qed.