proposition: Lemma ap_pr2CE (c := cons T1bad 1 zero): (forall a b, T1nf a -> T1nf b -> a < c -> b < c -> a + b < c).
proof: Proof. move => a b na nb; rewrite /c. move: na nb;case: a; first by rewrite T1add0n. move => a' n' b' HA; case: b; first by rewrite T1addn0. move => a'' n'' b'' HB. have pa: (a' == T1bad) = false. by apply /negP => /eqP ba; move: HA; rewrite ba /=. have pb: (a'' == T1bad) = false. by apply /negP => /eqP ba; move: HB; rewrite ba /=. rewrite /= !(fun_if (fun z => z < cons T1bad 1 zero)) /= pa pb => sa sb. by case (T1ltgtP a' a''). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)