proposition: Lemma Cle_le_S_eq : forall p q : nat, p <= q -> {S p <= q} + {p = q}.
proof: Proof. intros p q H. elim (gt_eq_gt_dec p q); intro H0. elim H0; auto. exfalso. apply Nat.lt_nge with q p; auto. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)