proposition: Lemma dicho_aux_le_xOXO : forall p:positive , xO (dicho_aux p) <= p -> xO (dicho_aux (p~0~0)) <= p~0~0.
proof: Proof. intros; rewrite dicho_aux_xOxO. red;rewrite Pos.compare_xO_xO. fold (xO(dicho_aux p) <= p~0). transitivity p; auto. clear H;red; change (p~0) with (2 * p); change p with (1 * p) at 1; rewrite Pos.mul_compare_mono_r; discriminate. Qed.
imports: Coq(Arith NArith)