proposition: Lemma Zmult_addr : right_distributive Zmult Zplus.
proof: Proof. exact: Zmult_plus_distr_r. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrnat seq order) mathcomp(choice fintype finfun ssrfun bigop ssralg) Zbool Qcanon ZArith