proposition: Lemma eq_add_pred : forall n m : nat, pred n = pred m -> {n = m} + {n < 2 /\ m < 2}.
proof: Proof. intros [|[|n]] m; simpl; intros H; try (right; lia); left; rewrite (f_equal S H); apply (Nat.lt_succ_pred 0); lia. Defined.
imports: Coq(ZArith) Coq(Lia)