proposition: Lemma equation_cartesienne_alignes : forall (M : PO) (x y a b c : R), x = abscisse M -> y = ordonnee M -> ~ (a = 0 /\ b = 0) -> a * x + (b * y + c) = 0 -> exists A : _, (exists B : _, A <> B /\ alignes A B M).
proof: Proof. intros M x y a b c 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 ]. cut (a <> 0 \/ b <> 0); intros. elim H2; intros. elim existence_representant_comb_lin_vecteur with (A := O) (B := I) (C := O) (D := J) (a := - c / a) (b := 0); [ intros A H4; try clear existence_representant_comb_lin_vecteur; try exact H4 ]. elim existence_representant_comb_lin_vecteur with (A := O) (B := I) (C := O) (D := J) (a := - b + - c / a) (b := a); [ intros B H6; try clear existence_representant_comb_lin_vecteur; try exact H6 ]. exists A; exists B. cut (vec A B = add_PP (mult_PP (- b) (vec O I)) (mult_PP a (vec O J))); intros. cut (A <> B); intros. split; [ try assumption | idtac ]. apply determinant_nul_alignement; auto. cut (vec A M = add_PP (mult_PP (x + c / a) (vec O I)) (mult_PP y (vec O J))); intros. rewrite (determinant_def (A:=A) (B:=B) (C:=A) (D:=M) (x:=- b) (y:=a) (x':= x + c / a) (y':=y)); auto. RReplace 0 (-0). rewrite <- H1; auto. RReplace (- b * y + - (a * (x + c / a))) (- (b * y + a * (x + c / a))). unfold Rdiv in |- *. RReplace (a * (x + c * / a)) (a * x + c * (a * / a)). RReplace (a * / a) 1. ring. RReplace (x + c / a) (x + - (- c / a)). RReplace y (y + -0). apply composantes_vecAB; eauto with geo. unfold Rdiv in |- *. ring. contrapose H3. rewrite H7 in H4. elim unicite_coordonnees with (O := O) (I := I) (J := J) (M := B) (x := - b + - c / a) (y := a) (x' := - c / a) (y' := 0); [ intros H9 H10; try clear unicite_coordonnees; try exact H10 | auto with geo | auto | auto ]. RReplace (- b) (- b + - c / a + - (- c / a)). pattern a at 3 in |- *. RReplace a (a + -0). apply composantes_vecAB; eauto with geo. elim existence_representant_comb_lin_vecteur with (A := O) (B := I) (C := O) (D := J) (a := 0) (b := - c / b); [ intros A H4; try clear existence_representant_comb_lin_vecteur; try exact H4 ]. elim existence_representant_comb_lin_vecteur with (A := O) (B := I) (C := O) (D := J) (a := - b) (b := a + - c / b); [ intros B H6; try clear existence_representant_comb_lin_vecteur; try exact H6 ]. exists A; exists B. cut (vec A B = add_PP (mult_PP (- b) (vec O I)) (mult_PP a (vec O J))); intros. cut (A <> B); intros. split; [ try assumption | idtac ]. apply determinant_nul_alignement; auto. cut (vec A M = add_PP (mult_PP x (vec O I)) (mult_PP (y + c / b) (vec O J))); intros. rewrite (determinant_def (A:=A) (B:=B) (C:=A) (D:=M) (x:=- b) (y:=a) (x':=x) (y':=y + c / b)); auto. RReplace 0 (-0). rewrite <- H1; auto. RReplace (- b * (y + c / b) + - (a * x)) (- (b * (y + c / b) + a * x)). unfold Rdiv in |- *. RReplace (b * (y + c * / b)) (b * y + c * (b * / b)). RReplace (b * / b) 1. ring. RReplace (y + c / b) (y + - (- c / b)). RReplace x (x + -0). apply composantes_vecAB; eauto with geo. unfold Rdiv in |- *. ring. contrapose H3. rewrite H7 in H4. elim unicite_coordonnees with (O := O) (I := I) (J := J) (M := B) (x := - b) (y := a + - c / b) (x' := 0) (y' := - c / b); [ intros H9 H10; try clear unicite_coordonnees; try exact H10 | auto with geo | auto | auto ]. RReplace 0 (-0). rewrite <- H9; ring. RReplace (- b) (- b + -0). RReplace a (a + - c / b + - (- c / b)). apply composantes_vecAB; eauto with geo. apply not_and_or; auto. Qed.