proposition: Lemma plus_pred_pred_plus : forall i j k, k <= pred i + pred j -> k <= pred (i + j).
proof: Proof. intros; lia. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)