proposition: Lemma eqrP : Equality.axiom eqr.
proof: Proof. by move=> r1 r2; rewrite /eqr; case: Req_EM_T=> H; apply: (iffP idP). Qed.
imports: Coq(Rdefinitions Raxioms RIneq Rbasic_fun) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq bigop)