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