proposition: Lemma phi0_ltR : forall a b, lt (phi0 a) (phi0 b) -> lt a b.
proof: Proof. intros c c' H; case (lt_inv H). - trivial. - intros [(_, i) | (_, (_, i))]; inversion i. 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)