proposition: Lemma ap_pr4 x: (forall b, b < x -> b + x = x) -> (x == zero) || T1ap x.
proof: Proof. case: x => // a; case; [ case => // a' n' b' H | move => n b H]. have: cons a 0 zero < cons a 0 (cons a' n' b') by rewrite /= T1ltnn eqxx. move /H;rewrite /= T1ltnn; discriminate. have: cons a n zero < cons a n.+1 b by rewrite /= T1ltnn eqxx ltnSn. by move /H; rewrite /= T1ltnn - {3} (addn0 n); case => /eqP; rewrite eqn_add2l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)