proposition: Lemma Zmultq0 : forall (q : Z), Zmult q 0%Z = 0%Z.
proof: Proof. exact: Zmult_0_r. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrnat seq order) mathcomp(choice fintype finfun ssrfun bigop ssralg) Zbool Qcanon ZArith