proposition: Lemma sub_pr a b: T1nf b -> (a + b) - a = b.
proof: Proof. elim: a b; first by move => b _; rewrite T1sub0. move => a' _ n' b' Hb; case; first by rewrite T1addn0 T1subnn. move => a n b nb /=. case (T1ltgtP a' a) => pa. by rewrite /= pa (T1lt_anti pa) (T1lt_ne' pa). have hh: a' == zero = false by move: pa; case a' => //; rewrite T1ltn0. by rewrite /= !T1ltnn ltnn !eqxx /= T1ltNge add_le1 hh /= Hb. rewrite /= T1ltnn eqxx - addnS addKn addnC eqn_simpl1 ltn_simpl1 pa. by move: nb; case: eqP => // -> nb; rewrite (T1nf_finite nb). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)