proposition: Lemma add_opp_diag_r n : n + - n = 0.
proof: Proof. destruct n; simpl; trivial; now rewrite pos_sub_diag. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass