proposition: Lemma consAD_orient_consAV: forall A B C M N P :PO, double_AV (cons_AV (vec A B)(vec A C))= double_AV (cons_AV (vec M N) (vec M P))-> orient A B C -> orient M N P -> cons_AV (vec A B) (vec A C) = cons_AV (vec M N) (vec M P).
proof: Proof. intros A B C M N P H H0 H1. unfold double_AV in H. deroule_orient H0. deroule_orient H1. destruct (tout_angle_a_une_mesure (A:=A) (B:=B) (C:=A) (D:=C)) as [x H15]; auto with geo. destruct (tout_angle_a_une_mesure (A:=M) (B:=N) (C:=M) (D:=P)) as [y H16]; auto with geo. rewrite <-H15 in *. rewrite <-H16 in *. rewrite <-add_mes_compatible in H. rewrite <-add_mes_compatible in H. replace (x+x) with (2*x) in H. replace (y+y) with (2*y) in H. cut (sin x = sin y). intros H17. cut (cos x = cos y). intros H18. apply egalite_angle_trigo;auto. assert (H19:sin (2*x) = sin (2*y)) by (apply sin_deux_mes;auto). repeat rewrite duplication_sin in H19. rewrite H17 in H19. apply Rmult_eq_reg_l with (r:=sin y). apply Rmult_eq_reg_l with (r:=2);auto with real. apply Rgt_not_eq. rewrite (@egalite_sin_Sin M N P y);auto. apply orient_SinusPositif;auto. assert (H19:cos (2*x) = cos (2*y)) by (apply cos_deux_mes;auto). repeat rewrite duplication_cos2 in H19. apply Rsqr_inj. assert (sin x >0) by (rewrite (@egalite_sin_Sin A B C x);auto; apply orient_SinusPositif;auto). lra. assert (sin y >0) by (rewrite (@egalite_sin_Sin M N P y);auto; apply orient_SinusPositif;auto). lra. apply Rmult_eq_reg_l with (r:=2);auto with real. assert (-(2*Rsqr (sin x)) = -((2*Rsqr (sin y)))) by (apply Rplus_eq_reg_l with (r:=1);auto with real). replace (2 * Rsqr(sin x)) with (-(-(2 * Rsqr(sin x))));auto with real. replace (2 * Rsqr(sin y)) with (-(-(2 * Rsqr(sin y))));auto with real. ring. ring. Qed.