proposition: Lemma unitZPl : forall x y, y * x = 1 -> Zunit x.
proof: Proof. move=> x y; rewrite mulrC. rewrite -[x * y]/(Zmult x y); move/Zmult_1_inversion_l. by case=> ->. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrnat seq order) mathcomp(choice fintype finfun ssrfun bigop ssralg) Zbool Qcanon ZArith