proposition: Remark P0 : P 0.
proof: Proof. repeat split. - intros x y; cbn; auto with arith. - apply smono_Sle. + discriminate. + intros x y; cbn; auto with arith. - intro n; simpl (Ack 1); cbn; induction n; cbn; auto with arith. Qed.
imports: Coq(Lia) Coq(Program.Wf Arith) hydras(ssrnat_extracts) Equations(Equations)