proposition: Lemma limit_is_lub_0 : forall i alpha, (forall j, (i,j) o< alpha) <-> (S i, 0) o<= alpha.
proof: Proof. intros i (k,l) ;split; intro H . - destruct (lt_eq_lt_dec (S i, 0) (k,l)) as [[Hlt | Heq] | Hgt]. + now left. + rewrite Heq; now right. + destruct (limitb_limit (S i,0)) as [H1 H2]. * red; trivial. * simpl in H1; destruct (H2 _ Hgt) as [x H0]. simpl in H0. specialize (H x). destruct (ON_mult.lt_strorder Omega Omega) as [H3 H4]. destruct (H3 (k,l)). transitivity (i,x); auto. - inversion_clear H. + inversion_clear H0. * intro. left. abstract lia. * left; left; auto. + left;left;auto. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Simple_LexProd ON_Generic ON_mult ON_Omega Compat815)