proposition: Fact inv_out : {in predC (predC1 0), inv =1 id}.
proof: Proof. by move=> x /negbNE/eqP->; exact: invr0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)