proposition: Lemma inj_sub_max n m : Z.of_N (n-m) = Z.max 0 (Z.of_N n - Z.of_N m).
proof: Proof. destruct n as [|n], m as [|m]; simpl; trivial. rewrite Z.pos_sub_spec, Pos.compare_sub_mask. unfold Pos.sub. now destruct (Pos.sub_mask n m). Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat