proposition: Theorem phi_spec1 a b c: c < a -> phi c (phi a b) = phi a b.
proof: Proof. move => ca; move: (phi_ap a b) (phi_le1 a b); case: (phi a b) => //. by move => a' b' n' c' /= [ -> ->] /= aa; rewrite (T2lt_le_trans ca aa). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)