proposition: Theorem sub_succ_r n m : n - succ m = pred (n - m).
proof: Proof. destruct n as [|p], m as [|q]; trivial. - now destruct p. - simpl. rewrite Pos.sub_mask_succ_r, Pos.sub_mask_carry_spec. now destruct (Pos.sub_mask p q) as [|[r|r|]|]. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties