proposition: Lemma aire_coordonnees : forall (M N : PO) (x y x' y' : R), vec O M = add_PP (mult_PP x (vec O I)) (mult_PP y (vec O J)) -> vec O N = add_PP (mult_PP x' (vec O I)) (mult_PP y' (vec O J)) -> aire (vec O M) (vec O N) = x * y' + - (y * x').
proof: Proof. intros. rewrite H. elim existence_representant_mult_vecteur with (A := O) (B := O) (C := I) (k := x); [ intros A H1; rewrite <- H1 ]. elim existence_representant_mult_vecteur with (A := O) (B := O) (C := J) (k := y); [ intros B H2; rewrite <- H2 ]. rewrite aire_distrib_r. rewrite H1. rewrite aire_colineaire_l. rewrite H2. rewrite aire_colineaire_l. rewrite H0. elim existence_representant_mult_vecteur with (A := O) (B := O) (C := I) (k := x'); [ intros C H3; rewrite <- H3 ]. elim existence_representant_mult_vecteur with (A := O) (B := O) (C := J) (k := y'); [ intros D H4; rewrite <- H4 ]. repeat rewrite aire_distrib_l. rewrite H3. repeat rewrite aire_colineaire_r. rewrite H4. repeat rewrite aire_colineaire_r. repeat rewrite aire_ABAB. rewrite unite_aire. rewrite opp_unite_aire. ring. Qed.