proposition: Lemma eq_creal_cst x y : reflect (cst_creal x == cst_creal y) (x == y).
proof: Proof. apply: (iffP idP)=> [|eq_xy]; first by move/eqP->. by apply/negP=> /negP /neq_creal_cst; rewrite eq_xy; apply: eq_creal_refl. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)