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