proposition: Lemma ROND_new : forall O I J K : PO, repere_orthonormal_direct O I J -> vec O K = mult_PP (-1) (vec O I) -> repere_orthonormal_direct O J K.
proof: Proof. unfold repere_orthonormal_indirect, repere_orthonormal_direct in |- *. intros O I J K H H0; try assumption. elim H; intros H1 H2; elim H2; intros H3 H4; try clear H2 H; try exact H4. cut (scalaire (vec O K) (vec O K) = 1); intros. split; [ auto | split; [ auto | try assumption ] ]. replace pisurdeux with (- pisurdeux + pi). cut (image_angle (- pisurdeux) = cons_AV (vec O J) (vec O I)); intros. cut (image_angle pi = cons_AV (vec O I) (vec O K)); intros. rewrite add_mes_compatible. rewrite H5; rewrite H2; rewrite Chasles; auto with geo. replace (vec O K) with (vec I O). rewrite <- angle_plat; auto with geo. rewrite H0. unfold vec in |- *; RingPP. apply mes_oppx; auto with geo. unfold pi in |- *; ring. rewrite H0. Simplscal; rewrite H3; ring. Qed.