proposition: Lemma equation_cartesienne_orthogonal : 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 /\ orthogonal (vec A B) (vec A 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 := a + - c / a) (b := 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 a (vec O I)) (mult_PP b (vec O J))); intros. cut (A <> B); intros. split; [ try assumption | idtac ]. cut (scalaire (vec A B) (vec A M) = 0); auto with geo. cut (vec A M = add_PP (mult_PP (x + c / a) (vec O I)) (mult_PP y (vec O J))); intros. elim existence_representant_vecteur with (A := O) (B := A) (C := B); [ intros N H21 ]. elim existence_representant_vecteur with (A := O) (B := A) (C := M); [ intros P H22 ]. rewrite <- H21; rewrite <- H22. rewrite (scalaire_coordonnees (O:=O) (I:=I) (J:=J) (M:=N) (N:=P) (x:=a) (y:=b) (x':=x + c / a) (y':=y)); auto with geo. rewrite <- H1; auto. unfold Rdiv in |- *. RReplace (a * (x + c * / a)) (a * x + c * (a * / a)). RReplace (a * / a) 1. ring. rewrite H21; auto. rewrite H22; auto. 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. RReplace a (a + - c / a + - (- c / a)). cut (a + - c / a = - c / a); intros. rewrite H8. unfold Rdiv in |- *. ring. elim unicite_coordonnees with (O := O) (I := I) (J := J) (M := B) (x := a + - c / a) (y := b) (x' := - c / a) (y' := 0); [ intros H9 H10; try clear unicite_coordonnees; try exact H9 | auto with geo | auto | auto ]. RReplace b (b + -0). RReplace a (a + - c / a + - (- c / a)). 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 := a) (b := b + - 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 a (vec O I)) (mult_PP b (vec O J))); intros. cut (A <> B); intros. split; [ try assumption | idtac ]. cut (scalaire (vec A B) (vec A M) = 0); auto with geo. cut (vec A M = add_PP (mult_PP x (vec O I)) (mult_PP (y + c / b) (vec O J))); intros. elim existence_representant_vecteur with (A := O) (B := A) (C := B); [ intros N H21 ]. elim existence_representant_vecteur with (A := O) (B := A) (C := M); [ intros P H22 ]. rewrite <- H21; rewrite <- H22. rewrite (scalaire_coordonnees (O:=O) (I:=I) (J:=J) (M:=N) (N:=P) (x:=a) (y:=b) (x':=x) (y':=y + c / b)); auto with geo. rewrite <- H1; auto. unfold Rdiv in |- *. RReplace (b * (y + c * / b)) (b * y + c * (b * / b)). RReplace (b * / b) 1. ring. rewrite H21; auto. rewrite H22; auto. 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. RReplace b (b + - c / b + - (- c / b)). cut (b + - c / b = - c / b); intros. rewrite H8. unfold Rdiv in |- *. ring. elim unicite_coordonnees with (O := O) (I := I) (J := J) (M := B) (x := a) (y := b + - c / b) (x' := 0) (y' := - c / b); [ intros H9 H10; try clear unicite_coordonnees; try exact H10 | auto with geo | auto | auto ]. RReplace a (a + -0). RReplace b (b + - c / b + - (- c / b)). apply composantes_vecAB; eauto with geo. apply not_and_or; auto. Qed.