proposition: Lemma succ_double_mul n m : succ_double n * m = double n * m + m.
proof: Proof. destruct n; simpl; destruct m; trivial. now rewrite Pos.add_comm. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties