proposition: Lemma ap_pr0 a (x := phi0 a) b c: b < x -> c < x -> b + c < x.
proof: Proof. case: b c; [by move => c |move => a1 n b]. case; [by move => H _ | move => a' n' c']. by rewrite ! (fun_if (fun z => z < x)) !phi0_lt1 if_same; case: (a1 < a'). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)