proposition: Lemma pos_sub_gt p q : (q < p)%positive -> pos_sub p q = pos (p - q).
proof: Proof. intros H. now rewrite pos_sub_spec, Pos.compare_antisym, H. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass