proposition: Lemma triangle_rectangle_repere : forall O I J : PO, O <> I -> O <> J -> orthogonal (vec O I) (vec O J) -> repere_orthogonal O I J.
proof: Proof. intros; red in |- *. cut (scalaire (vec O I) (vec O J) = 0); intros. split; [ idtac | try assumption ]. red in |- *; red in |- *; red in |- *; intros. halignes H3 k. rewrite H4 in H2. rewrite scalaire_mult_d in H2. elim (classic (k = 0)); intros. rewrite H5 in H4. absurd (O = J); auto. apply vecteur_nul_conf. rewrite H4; Ringvec. absurd (O = I); auto. apply distance_nulle. elim Rmult_integral with (r1 := k) (r2 := scalaire (vec O I) (vec O I)); [ intros H6; try clear without_div_Od | intros H6; try clear without_div_Od; try exact H6 | auto ]. absurd (k = 0); auto. apply def_orthogonal; auto. Qed.