proposition: Lemma T1F_inj: injective T1nat.
proof: Proof. case; first by case => //; discriminate. move => n; case; [discriminate | by move => m; case => ->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)