proposition: Lemma nf_add a b: T1nf a -> T1nf b -> T1nf (a + b).
proof: Proof. elim: a b => // a Ha n b Hb [] // a' n' b' ha hb /=. case (T1ltgtP a a') => //;last by move => ->; move: hb. rewrite -(phi0_lt1 _ n' b') => pb. by move: ha => /= /and3P [-> sb sc]; rewrite (Hb _ sb hb) ap_pr0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)