proposition: Lemma F_restricted_mono_l alpha beta n: Canon_plus n alpha beta -> (F_ beta n <= F_ alpha n)%N.
proof: Proof. rewrite /Canon_plus /F_. move => HCanon; apply /leP. by apply F_restricted_mono_l. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec Arith) hydras(DecPreOrder) hydras(T1 E0) hydras(primRec) hydras(F_alpha F_omega) gaia_hydras(T1Bridge GCanon GHprime)