proposition: Lemma ap_pr0 a b (x := [a,b]) u v: u < x -> v < x -> u + v < x.
proof: Proof. case: u v; [by move => u |move => a1 b1 n1 c1]. case; [by move => H _ | move => a' b' n' c' l1 l2 /=]. have aux: forall n' d', cons a1 b1 n' d' < x. by move => n'' d'';move: l1;rewrite psi_lt1 psi_lt1. by case: (T2ltgtP [a1, b1] [a', b']). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)