proposition: Lemma determinant_distrib_l : forall A B C D E F : PO, det (vec A B) (add_PP (vec C D) (vec E F)) = det (vec A B) (vec C D) + det (vec A B) (vec E F).
proof: Proof. intros. elim existence_representant_som_vecteur with (A := C) (B := D) (C := E) (D := F); [ intros G H; try clear existence_representant_som_vecteur; rewrite <- H ]. repeat rewrite determinant_aire. rewrite H. apply aire_distrib_l. Qed.