proposition: Remark Le_iff : forall alpha beta, E0le alpha beta <-> T1.LE (@cnf alpha) (@cnf beta).
proof: Proof. intros *; unfold E0le, T1.LE; destruct alpha, beta; split. - cbn; rewrite le_lt_eq; destruct 1. + red in H; cbn in H; repeat split; auto; apply LE_le; repeat split; auto. destruct H as [H [H0 _]]. now left. + repeat split; auto. injection H; intro; subst; right. - cbn; destruct 1 as [_ [H _]]; rewrite le_lt_eq in H. destruct H. + left; red; cbn; repeat split; auto. + subst; cbn; unfold E0lt. generalize (E0_eq_intro {| cnf := cnf1; cnf_ok := cnf_ok0 |} {| cnf := cnf1; cnf_ok := cnf_ok1 |}). cbn; intro H; rewrite H. * now right. * reflexivity. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles ArithRing Wellfounded Operators_Properties Logic.Eqdep_dec) hydras(Prelude.More_Arith Prelude.Restriction Prelude.DecPreOrder ON_Generic OrdNotations)