proposition: Lemma opp_add_distr n m : - (n + m) = - n + - m.
proof: Proof. destruct n, m; simpl; trivial using pos_sub_opp. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass