proposition: Theorem inj_sub_max p q : to_nat (p - q) = Nat.max 1 (to_nat p - to_nat q).
proof: Proof. destruct (ltb_spec q p) as [H|H]. - rewrite <- inj_sub by trivial. now destruct (is_succ (p - q)) as (m,->). - rewrite sub_le by trivial. apply inj_le, Nat.sub_0_le in H. now rewrite H. Qed.
imports: BinPos PeanoNat