proposition: Lemma dicho_aux_le_xOXI : forall p:positive , xO (dicho_aux p) <= p -> xO (dicho_aux (p~0~1)) <= p~0~1.
proof: Proof. intros; rewrite dicho_aux_xIxO. 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; change p with (1 * p) at 1; red;rewrite Pos.mul_compare_mono_r; discriminate. - clear H; induction p; simpl;[auto | auto | discriminate ]. Qed.
imports: Coq(Arith NArith)