proposition: Lemma add_assoc n m p : n + (m + p) = n + m + p.
proof: Proof. destruct n. - trivial. - apply add_assoc_pos. - apply opp_inj. rewrite !opp_add_distr. simpl. apply add_assoc_pos. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass