proposition: Lemma mulC_id : left_id one mul -> right_id one mul.
proof: Proof. by move=> mul1x x; rewrite mulC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)