proposition: Lemma ap_pr1 c: (forall a b, a < c -> b < c -> a + b < c) -> (c== zero) || T1ap c.
proof: Proof. case: c => // a n b. case: n b => [b H | n b H]; last first. have l2: (cons a n b) < (cons a n.+1 b) by rewrite /= eqxx ltnS leqnn if_same. move: (H _ _ l2 l2); rewrite /= !T1ltnn /= !T1ltnn eqxx if_same. by rewrite ltnS -{3}(add0n n) ltn_add2r. case bz: (b == zero) => //. have pa: cons a 0 zero < cons a 0 b by move: bz;rewrite /= !T1ltnn eqxx; case b. by move: (H _ _ pa pa); rewrite /= T1ltnn /= T1ltnn if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)