proposition: Lemma mulC_dist : left_distributive mul add -> right_distributive mul add.
proof: Proof. by move=> mul_addl x y z; rewrite !(mulC x). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)