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