proposition: Lemma unitrP (x y : U) : y * x = 1 /\ x * y = 1 -> val x \is a unit.
proof: Proof. move=> -[/(congr1 val) yx1 /(congr1 val) xy1]. by apply: rev_unitrP (val y) _; rewrite !rmorphM rmorph1 /= in yx1 xy1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)