proposition: Theorem S_predn : forall m : nat, m <> 0 -> S (pred m) = m.
proof: Proof. intros m H. symmetry in |- *. symmetry; apply Nat.lt_succ_pred with 0. lia. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)