proposition: Lemma non_produit_un : forall k k' : R, k' * k <> 1 -> 1 + - (k' * k) <> 0.
proof: Proof. intros; red in |- *; intros. apply H. replace 1 with (1 + - (k' * k) + k' * k); [ idtac | ring ]. rewrite H0; ring. Qed.