proposition: Lemma phi0_mono : forall a b, leq lt a b -> leq lt (phi0 a) ( phi0 b).
proof: Proof. intros * ; rewrite !le_lt_eq. destruct 1 as [Hlt | Heq]. - left; now apply phi0_mono_strict. - subst; now right. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)