proposition: Lemma pos_sub_opp p q : - pos_sub p q = pos_sub q p.
proof: Proof. revert q; induction p as [p IHp|p IHp|]; intros q; destruct q; simpl; trivial; rewrite <- IHp; now destruct pos_sub. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass