proposition: Lemma opp_inj n m : -n = -m -> n = m.
proof: Proof. destruct n, m; simpl; intros H; destr_eq H; now f_equal. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass