proposition: Fact pair_mul1r : right_id (1, 1) mul_pair.
proof: Proof. by case=> x1 x2; congr (_, _); apply: mulr1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)