proposition: Lemma ZmulV : {in Zunit, left_inverse 1%R Zinv *%R}.
proof: Proof. by move=> x; rewrite inE; case/pred2P => ->. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrnat seq order) mathcomp(choice fintype finfun ssrfun bigop ssralg) Zbool Qcanon ZArith