proposition: Lemma nf_add a b: T2nf a -> T2nf b -> T2nf (a + b).
proof: Proof. have psi1: forall a' b' n' c' a b, cons a' b' n' c' < [a,b] = ([a', b'] < [a,b]). move => a' b' n' c' a'' b''. by rewrite T2lt_consE T2ltn0 ltn0 !if_same if_simpl T2lt_psi. elim: a b => // a Ha b Hb n c Hc [] // a' b' n' c' ha hb /=. case (T2ltgtP [a, b] [a', b']) => // h; last by move: hb; case:h => -> ->. move: ha; rewrite /T2nf -/T2nf => /and4P [sa sb sc sd]. rewrite sa sb Hc //=; move: sd; case c => //=; first by rewrite psi1. move => a1 b1 n1 c1; rewrite psi1. by case: (T2ltgtP [a1, b1] [a', b']) => //;rewrite psi1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)