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