proposition: Lemma sub_pr a b: T2nf b -> (a + b) - a = b.
proof: Proof. elim: a b; first by move => b _; rewrite T2subn0. move => a' _ b' _ n' c' Hc; case; first by rewrite T2addn0 T2subnn. move => a b n c nn /=. case (T2ltgtP [a', b'] [a, b]) => pa; rewrite /= T2lt_consE -T2lt_psi. + rewrite pa /= (T2lt_anti pa); case h: (_ && _) => //. by move: pa; move/andP: h => [/eqP -> /eqP ->]; rewrite T2ltnn. + rewrite !T2ltnn !eqxx /= ltnn (T2ltNge _ c') add_le1 /=. by rewrite Hc // ifF //; case: eqP => h //; move: pa; rewrite h T2lt1. + rewrite !T2ltnn !eqxx addnC ltn_simpl1 eqn_simpl1 - addSn addnK /=. move: pa nn; case => -> -> ; case: eqP => //; case => -> -> h. by rewrite (T2nf_finite _ h). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)