proposition: Lemma scalaire_non_nul : forall A B C : PO, A <> B -> alignes A B C -> scalaire (vec A C) (vec A C) = 1 -> scalaire (vec A B) (vec A C) >= 0 -> scalaire (vec A B) (vec A C) <> 0.
proof: Proof. intros. halignes H0 k. rewrite H3. replace (scalaire (vec A B) (mult_PP k (vec A B))) with (k * scalaire (vec A B) (vec A B)). cut (scalaire (vec A B) (vec A B) <> 0 /\ k <> 0); intros. cut (~ (k = 0 \/ scalaire (vec A B) (vec A B) = 0)); intros. unfold not in |- *; intros; apply H5. apply Rmult_integral; auto with *. tauto. split; [ try assumption | idtac ]. auto with geo. elim (classic (k = 0)); auto; intros. rewrite H4 in H3. rewrite H3 in H1. absurd (0 = 1); auto with *. rewrite <- H1. Simplscal. Simplscal. Qed.