proposition: Lemma nat_semi_ring : semi_ring_theory 0 1 addn muln (@eq _).
proof: Proof. exact: mk_srt add0n addnC addnA mul1n mul0n mulnC mulnA mulnDl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring