proposition: Lemma inj_sub_max p q : Z.pos (p - q) = Z.max 1 (Z.pos p - Z.pos q).
proof: Proof. simpl. rewrite Z.pos_sub_spec. case Pos.compare_spec; intros. - subst; now rewrite Pos.sub_diag. - now rewrite Pos.sub_lt. - now destruct (p-q)%positive. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass