proposition: Lemma add_no_neutral p q : q + p <> p.
proof: Proof. revert q. induction p as [p IHp|p IHp| ]; intros [q|q| ] H; destr_eq H; apply (IHp q H). Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef