proposition: Lemma aire_colineaire_l : forall (k : R) (A B C D : PO), aire (mult_PP k (vec A B)) (vec C D) = k * aire (vec A B) (vec C D).
proof: Proof. intros. discrimine A B. VReplace (mult_PP k (vec B B)) zero; auto with geo. VReplace (vec B B) zero; auto with geo. rewrite aire_vecteur_nul_l; ring. discrimine C D. VReplace (vec D D) zero; auto with geo. elim existence_representant_mult_vecteur with (A := A) (B := A) (C := B) (k := k); [ intros E H2; rewrite <- H2 ]. repeat rewrite aire_vecteur_nul_r; ring. elim existence_representant_mult_vecteur with (A := A) (B := A) (C := B) (k := k); [ intros E H2; rewrite <- H2 ]. discrimine k 0. replace (vec A E) with zero. ring_simplify; auto with geo. rewrite H2; rewrite H1; Ringvec. cut (A <> E); intros. elim existence_representant_vecteur with (A := A) (B := C) (C := D); [ intros F H4; rewrite <- H4; intros ]. cut (A <> F); intros. deroule_representant_unitaire A B G. deroule_representant_unitaire A F L. rewrite def_aire; auto. rewrite def_aire; auto. rewrite angles_representants_unitaires; auto. rewrite angles_representants_unitaires; auto. elim Rtotal_order with (r1 := k) (r2 := 0); [ intros H16; try clear total_order | intros H16; elim H16; [ intros H17; try clear H16 | intros H17; try clear H16; try exact H17 ] ]. rewrite (produit_negatif_representant_unitaire (k:=k) (A:=A) (B:=B) (C:=E)); auto. rewrite <- H11; rewrite <- H6. elim existence_representant_mult_vecteur with (A := A) (B := A) (C := G) (k := -1); [ intros K H17; try clear existence_representant_mult_vecteur; try exact H17 ]. mesure A G A L. rewrite H18; rewrite <- H17. rewrite <- (egalite_sin_Sin (A:=A) (B:=G) (C:=L) (x:=x)); auto. rewrite <- (egalite_sin_Sin (A:=A) (B:=K) (C:=L) (x:=pi + x)); auto. elim pi_plus_x with (x := x); [ intros H19 H20; try clear pi_plus_x; try exact H20 ]. rewrite H20. replace (distance A E) with (- k * distance A B). ring. symmetry in |- *. rewrite <- Rabs_left; auto with real. apply colinearite_distance; auto. apply distinct_produit_vecteur with (3 := H17); auto with real. replace (cons_AV (vec A K) (vec A L)) with (plus (cons_AV (vec A K) (vec A G)) (cons_AV (vec A G) (vec A L))). replace (vec A K) with (vec G A). rewrite <- angle_plat; auto. rewrite <- H18; rewrite <- add_mes_compatible; auto. rewrite H17; Ringvec. rewrite Chasles; auto. apply distinct_produit_vecteur with (3 := H17); auto with real. absurd (k = 0); auto. rewrite <- (produit_positif_representant_unitaire (k:=k) (A:=A) (B:=B) (C:=E)) ; auto. rewrite <- H11; rewrite <- H6. elim existence_representant_mult_vecteur with (A := A) (B := A) (C := G) (k := -1); [ intros K H18; try clear existence_representant_mult_vecteur ]. mesure A G A L. replace (distance A E) with (k * distance A B). ring. symmetry in |- *. rewrite <- (Rabs_right k); auto with real. apply colinearite_distance; auto. apply Rgt_ge; auto. apply distinct_egalite_vecteur with (2 := H4); auto. apply distinct_produit_vecteur with (3 := H2); auto with real. Qed.