proposition: Lemma alignes_equation_cartesienne : forall (A B M : PO) (x y : R), x = abscisse M -> y = ordonnee M -> A <> B -> alignes A B M -> exists a : R, (exists b : R, (exists c : R, a * x + (b * y + c) = 0 /\ ~ (a = 0 /\ b = 0))).
proof: Proof. intros A B M x y H20 H30 H0 H1; try assumption. cut (vec O M = add_PP (mult_PP x (vec O I)) (mult_PP y (vec O J))); [ intros H | auto with geo ]. elim composantes_vecteur with (O := O) (I := I) (J := J) (M := A) (N := B); [ intros a H2; elim H2; [ intros b H3; try clear H2; try exact H3 ] | auto with geo ]. elim existence_coordonnees with (O := O) (I := I) (J := J) (M := A); [ intros x0 H2; elim H2; [ intros y0 H4; try clear H2; try exact H4 ] | auto with geo ]. cut (vec A M = add_PP (mult_PP (x + - x0) (vec O I)) (mult_PP (y + - y0) (vec O J))); intros. 2: apply composantes_vecAB; eauto with geo. exists (- b); exists a; exists (b * x0 + - (a * y0)). split; [ try assumption | idtac ]. rewrite <- (alignement_determinant (A:=A) (B:=B) (M:=M)); auto. rewrite (determinant_def (A:=A) (B:=B) (C:=A) (D:=M) (x:=a) (y:=b) (x':= x + - x0) (y':=y + - y0)); auto. ring. contrapose H0. applatit_and. apply vecteur_nul_conf. rewrite H3. RReplace b (- - b). rewrite H6; rewrite H7; Ringvec. Qed.