proposition: Fact Z_of_intE (n : int) : Z_of_int n = (n%:~R)%R.
proof: Proof. have Hnat (m : nat) : Z.of_nat m = (m%:R)%R. by elim: m => // m; rewrite Nat2Z.inj_succ -Z.add_1_l mulrS => ->. case: n => n; rewrite /intmul /=; first exact: Hnat. by congr Z.opp; rewrite Nat2Z.inj_add /= mulrSr Hnat. Qed.
imports: Coq(ZArith) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop finset prime) mathcomp(order binomial ssralg countalg ssrnum ssrint) mathcomp(zify_ssreflect)