proposition: Lemma sub_pr a b: T3nf b -> (a + b) - a = b.
proof: Proof. elim: a b; first by move => b _; rewrite T3subn0. move => a' _ b' _ c' _ n' d' Hd; case; first by rewrite T3addn0 T3subnn. move => a b c n d nn /=. case (T3ltgtP [a', b', c'] [a, b, c]) => pa; rewrite /= T3lt_consE. by rewrite pa /= (T3lt_anti pa) (T3lt_ne' pa). rewrite !T3ltnn ltnn !eqxx (T3ltNge _ d') add_le1 /=. by rewrite Hd // ifF //; case: eqP => h //; move: pa; rewrite h T3lt1. rewrite !T3ltnn !eqxx addnC ltn_simpl1 eqn_simpl1 - addSn addnK /=. move: pa nn; case => -> -> ->; case: eqP => //; case => -> -> ->. by rewrite /T3nf T3lt1 /= => /andP[_ /eqP ->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)