proposition: Lemma Pos_pred_double_inj: forall (p q : positive), Pos.pred_double p = Pos.pred_double q -> p = q.
proof: Proof. intros p q H. apply (f_equal Pos.succ) in H. do 2 rewrite Pos.succ_pred_double in H. inversion H; reflexivity. Qed.
imports: ZArith ConstructiveEpsilon