proposition: Remark H'_non_mono1 : ~ (forall alpha beta k, (alpha o<= beta)%e0 -> (H'_ alpha k <= H'_ beta k)%nat).
proof: Proof. intros H ;specialize (H 42 E0_omega 3). assert (H0 :(42 o<= E0_omega)%e0). { repeat split; auto. compute. now left. } apply H in H0; rewrite H'_Fin, H'_omega in H0; abstract lia. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)