proposition: Lemma natr_mul_eq1 x y : x \is a nat_num -> y \is a nat_num -> (x * y == 1) = (x == 1) && (y == 1).
proof: Proof. by do 2!move/truncK <-; rewrite -natrM !pnatr_eq1 muln_eq1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)