proposition: Lemma mulC_zero : left_zero zero mul -> right_zero zero mul.
proof: Proof. by move=> mul0x x; rewrite mulC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)