proposition: Lemma ap_pr2CE (c := cons zero zero T3bad 1 zero): (forall a b, T3nf a -> T3nf b -> a < c -> b < c -> a + b < c).
proof: Proof. move => a b na nb. have aux: forall a' b' c' n' d', cons a' b' c' n' d' < c = if (a'==zero) && (b'==zero) then if (c' < T3bad) then true else if (c'==T3bad) then n'==0 else false else ([a', b', c'] < T3bad). move => a' b' c' n' d'. rewrite /c T3lt_consE T3ltn0 !if_same if_simpl ltnS leqn0 T3eqE !eqxx. rewrite T3lt_psi /lt_psi !T3ltn0 !T3lt0n !andbF /=. case pa: (a'==zero) => /=; last by rewrite T3eqE pa /= orbF if_simpl. case pb: (b'==zero); last by rewrite T3eqE pb andbF /= orbF if_simpl. by case : (T3ltgtP c' T3bad). move: na nb;case: a; first by rewrite T3add0n. move => a' b' c' n' d' HA; case: b; first by rewrite T3addn0. move => a'' b'' c'' n'' d'' _. rewrite aux. case pa: ((a' == zero) && (b' == zero)); last first. move => H; rewrite aux. case pa': ((a'' == zero) && (b'' == zero)) => H' /=; by case: (T3ltgtP [a', b', c'] [a'', b'', c'']) => sa; rewrite aux ?pa ?pa'. move => pb; rewrite aux. case pa': ((a'' == zero) && (b'' == zero)) => H' /=; last first. case: (T3ltgtP [a', b', c'] [a'', b'', c'']) => pb'; rewrite aux ?pa ?pa' //. move: pb; case: (T3ltgtP c' T3bad) => // ww. by move: pa pa'; case: pb' => -> -> _ ->. move/andP: pa => [/eqP -> /eqP ->]. move/andP: pa' => [/eqP -> /eqP ->]. rewrite !T3lt_psi /lt_psi eqxx T3ltnn /= !orbF. case: (T3ltgtP c' c'') => h; rewrite aux => //=. move:pb;case: (T3ltgtP c' T3bad) => // ww. by move: HA; rewrite /T3nf ww /T3bad /T3nf -/T3nf T3ltnn !andbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)