proposition: Lemma sub_le1 a b : T1nf a -> (a - b) <= a.
proof: Proof. elim: a b => [b // | a' _ n' b' Hb]. case; [by rewrite T1sub0 T1lenn | move => a n b /and3P [_ /Hb la lb] /=]. set u := if a' <a then _ else _; case: u => //. case: (a < a') => //; case: (ltngtP n' n) => // nn. have hh: ((n' - n).-1 < n')%N. move: nn; by case: n' => // n' h; rewrite subSn // ltnS leq_subr. rewrite (fun_if (fun z => (z <= _))) !T1le_consE T1ltnn hh eqxx (eq_sym _ a'). by case (T1ltgtP a' zero). case :eqP => // _. apply: (T1le_trans (la b));exact:(T1ltW (tail_lt_cons n' lb)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)