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