proposition: Lemma double_add n m : double (n+m) = double n + double m.
proof: Proof. now destruct n, m. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties