proposition: Lemma equilateral_non_alignes : forall A B C : PO, A <> B -> scalaire (vec A B) (vec A B) = scalaire (vec A C) (vec A C) -> scalaire (vec A B) (vec A B) = scalaire (vec B C) (vec B C) -> ~ alignes A B C.
proof: Proof. intros A B C H H0 H1; red in |- *; intros H2; try exact H2. halignes H2 k. rewrite H3 in H0. cut (vec B C = mult_PP (k + -1) (vec A B)); intros. rewrite H4 in H1. cut (k * k = 1); intros. cut ((k + -1) * (k + -1) = 1); intros. cut (k = 1 \/ k = -1); intros. elim H7; [ intros H8; try clear H7; try exact H8 | intros H8; try clear H7 ]. rewrite H8 in H6. absurd (0 = 1); auto with *. rewrite <- H6; ring. rewrite H8 in H6. absurd ((-1 + -1) * (-1 + -1) = 1). try discrR. try assumption. cut (k + -1 = 0 \/ k + 1 = 0); intros. elim H7; [ intros H8; try clear H7; try exact H8 | intros H8; try clear H7 ]. left; try assumption. replace k with (k + -1 + 1). rewrite H8; ring. ring. right; try assumption. replace k with (k + 1 + -1). rewrite H8; ring. ring. apply Rmult_integral. replace 0 with (k * k + -1). ring. rewrite H5; ring. apply Rmult_eq_reg_l with (scalaire (vec A B) (vec A B)). replace (scalaire (vec A B) (vec A B) * 1) with (scalaire (vec A B) (vec A B)). pattern (scalaire (vec A B) (vec A B)) at 2 in |- *. rewrite H1. rewrite scalaire_mult_mult; ring. ring. unfold not in |- *; intros; apply H. apply distance_nulle; auto. apply Rmult_eq_reg_l with (scalaire (vec A B) (vec A B)). replace (scalaire (vec A B) (vec A B) * 1) with (scalaire (vec A B) (vec A B)). pattern (scalaire (vec A B) (vec A B)) at 2 in |- *. rewrite H0. rewrite scalaire_mult_mult; ring. ring. unfold not in |- *; intros; apply H. apply distance_nulle; auto. replace (vec B C) with (add_PP (vec A C) (mult_PP (-1) (vec A B))). rewrite H3. Ringvec. Ringvec. Qed.