proposition: Lemma nf_add a b: T3nf a -> T3nf b -> T3nf (a + b).
proof: Proof. elim: a b => // a Ha b Hb c Hc n d Hd [] // a' b' c' n' d' ha hb /=. case (T3ltgtP [a, b, c] [a', b', c']) => // h. move: ha; rewrite /T3nf -/T3nf => /and5P [sa sb sc sd se]. rewrite sa sb sc Hd //=; move: se; case d => //=; first by rewrite psi_lt1. move => a1 b1 c1 n1 d1; rewrite psi_lt1 => ha. case: (T3ltgtP [a1, b1, c1] [a', b', c']); rewrite psi_lt1 //. by move: hb; case:h => -> -> ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)