proposition: Lemma orient_SinusPositif : forall A B C :PO, orient A B C-> Sin (cons_AV (vec A B )(vec A C ))>0.
proof: Proof. intros A B C H. generalize H;intros H0. unfold orient in H0. rewrite def_aire in *;deroule_orient H;auto. elim (@distance_pos A B );intros H10 ; [idtac|elim (@distincts_dist_non_nulle A B H3);auto]. elim (@distance_pos A C );intros H11 ; [idtac|elim (@distincts_dist_non_nulle A C H5);auto]. assert (H9 :0< distance A C * Sin(cons_AV (vec A B )(vec A C)) ). apply Rmult_lt_reg_l with (r:= distance A B);auto with real. replace (distance A B *0) with 0 ;auto with real. red. apply Rmult_lt_reg_l with (r:= distance A C);auto with real. replace (distance A C *0) with 0 ;auto with real. Qed.