proposition: Lemma pair_unitP x y : y * x = 1 /\ x * y = 1 -> x \is a pair_unitr.
proof: Proof. case=> [[y1x y2x] [x1y x2y]]; apply/andP. by split; apply/unitrP; [exists y.1 | exists y.2]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)