proposition: Lemma nsatzR_diff: forall x y:R, not (x == y) -> not (x - y == 0).
proof: Proof. intros. intro; apply H. simpl; setoid_replace x with ((x - y) + y). - simpl. setoid_rewrite H0. simpl; cring. - simpl. simpl; cring. Qed.
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool Algebra_syntax Ncring Ncring_initial Ncring_tac Integral_domain ZArith Lia