proposition: Remark R1: forall n: nat, ~ Limit n.
proof: Proof. intros n [H H0]; destruct n. destruct H as [w Hw]; lia. destruct (H0 n) as [p Hp]; lia. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)