proposition: Lemma double_inj n m : double n = double m -> n = m.
proof: Proof. intro H. rewrite <- (div2_double n), H. apply div2_double. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties