proposition: Lemma pair_mulVr : {in pair_unitr, right_inverse 1 pair_invr *%R}.
proof: Proof. rewrite /pair_invr=> x; case: ifP => // /andP[Ux1 Ux2] _. by congr (_, _); apply: mulrV. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)