proposition: Lemma Req_dec : forall r1 r2, {r1 = r2} + {r1 <> r2}.
proof: Proof. intros r1 r2. destruct (total_order_T r1 r2) as [[Hlt|Heq]|Hgt]. right; intro Hn; apply (Rlt_irrefl r2); rewrite Hn in Hlt; assumption. left; assumption. right; intros Hn; apply (Rlt_irrefl r2); rewrite Hn in Hgt; assumption. Qed.
imports: RIneq MyNeq Rfunctions Lra