proposition: Lemma ap_pr3 a b (x := phi0 a): b < x -> b + x = x.
proof: Proof. by rewrite /x /phi0; case: b => // a' n' b'; rewrite phi0_lt1 /= => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)