proposition: Lemma sub_le1 a b : T3nf a -> (a - b) <= a.
proof: Proof. elim: a b => [b // | a' _ b' _ c' _ n' d' H]. case; [by rewrite T3subn0 T3lenn | move => a b c n d/and5P [_ _ _ /H la lb] /=]. have hh: (n < n')%N -> ((n' - n).-1 < n')%N. by case: n' => // n' h; rewrite subSn // ltnS leq_subr. rewrite T3lt_consE;case: (T3ltgtP [a', b', c'] [a, b, c]) => // eq1. case : (ltngtP n' n) => // eq2. case x1: ([a', b', c'] == one) => //. by rewrite /T3le T3lt_consE (eqP x1) T3ltnn eqxx hh // orbT. by rewrite /T3le T3lt_consE T3ltnn eqxx hh // orbT. case : (d' < d) => //; case: ([a', b', c'] ==one) => //. apply: (T3le_trans (la d)); apply:T3ltW; apply: (T3lt_le_trans lb). apply: T3le_psi. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)