proposition: Lemma sub_le1 a b : T2nf a -> (a - b) <= a.
proof: Proof. elim: a b => [b // | a' _ b' _ n' c' H]. case; [by rewrite T2subn0 T2lenn | move => a b n c/and4P [_ _ /H la lb] /=]. have hh: (n < n')%N -> ((n' - n).-1 < n')%N. by case: n' => // n' h; rewrite subSn // ltnS leq_subr. rewrite T2lt_consE -T2lt_psi; case: (T2ltgtP [a', b'] [a, b]) => // eq1. case sa: ((a' == a) && (b' == b)) => //. by move: eq1; move/andP:sa => [/eqP -> /eqP ->]; rewrite T2ltnn. case: eq1 => <- <- ; rewrite !eqxx /=. case : (ltngtP n' n) => // eq2. case x1: ([a', b'] == one);rewrite T2le_consE (hh eq2) ?eqxx. by move: x1; rewrite T2eqE => /and4P [/eqP -> /eqP ->] /=. by rewrite /= if_same. case : (c' < c) => //; case: ([a', b'] ==one) => //. apply: (T2le_trans (la c)); apply:T2ltW; apply: (T2lt_le_trans lb). apply: T2le_psi1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)