proposition: Theorem sub_succ_r : forall n m, n - (S m) == P (n - m).
proof: Proof. intros n m. zify. rewrite Zminus_mod_idemp_r, Zminus_mod_idemp_l. now replace ([|n|] - ([|m|] + 1))%Z with ([|n|] - [|m|] - 1)%Z by ring. Qed.
imports: NZAxioms ZArith Zpow_facts DoubleType CyclicAxioms Lia