proposition: Lemma Rneq_lt_or_gt: forall x y, x <> y -> {x < y} + {y < x}.
proof: Proof. intros x y x_neq_y. destruct (Rle_lt_dec x y). left ; apply Rneq_le_lt ; assumption. right ; assumption. Qed.
imports: RIneq MyNeq Rfunctions Lra