Require Import Reals.
Require Import DiscrR.

Lemma ex0 : 1%R <> 0%R.
Proof.
  discrR.
Qed.

Lemma ex1 : 0%R <> 2%R.
Proof.
  discrR.
Qed.
Lemma ex2 : 4%R <> 3%R.
Proof.
  discrR.
Qed.

Lemma ex3 : 3%R <> 5%R.
Proof.
  discrR.
Qed.

Lemma ex4 : (-1)%R <> 0%R.
Proof.
  discrR.
Qed.

Lemma ex5 : (-2)%R <> (-3)%R.
Proof.
  discrR.
Qed.

Lemma ex6 : 8%R <> (-3)%R.
Proof.
  discrR.
Qed.

Lemma ex7 : (-8)%R <> 3%R.
Proof.
  discrR.
Qed.