proposition: Lemma Reqb_eq : forall r1 r2, Reqb r1 r2 = true <-> r1=r2.
proof: Proof. intros; unfold Reqb; destruct Req_dec as [EQ|NEQ]; auto with *. split; try discriminate. intro EQ; elim NEQ; auto. Qed.
imports: Rbase Equalities Orders OrdersTac