proposition: Lemma pair_invr_out : {in [predC pair_unitr], pair_invr =1 id}.
proof: Proof. by rewrite /pair_invr => x /negPf/= ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)