proposition: Lemma Rneq_lt_gt_dec : forall a b, a <> b -> { a < b } + { b < a }.
proof: Proof. intros a b ab_neq ; destruct (Rlt_le_dec a b). left ; assumption. right ; apply Rle_neq_lt ; [| symmetry] ; assumption. Qed.
imports: RIneq MyNeq Rfunctions Lra