proposition: Lemma ldiff_le : forall a b, 0<=b -> ldiff a b == 0 -> 0 <= a <= b.
proof: Proof. assert (AUX : forall n, 0<=n -> forall a b, 0 <= a < 2^n -> 0<=b -> ldiff a b == 0 -> a <= b). { intros n Hn. apply le_ind with (4:=Hn); clear n Hn. - solve_proper. - intros a b Ha Hb _. rewrite pow_0_r, one_succ, lt_succ_r in Ha. setoid_replace a with 0 by (destruct Ha; order'); trivial. - intros n Hn IH a b (Ha,Ha') Hb H. assert (NEQ : 2 ~= 0) by order'. rewrite (div_mod a 2 NEQ), (div_mod b 2 NEQ). apply add_le_mono. + apply mul_le_mono_pos_l; try order'. apply IH. * split. { apply div_pos; order'. } apply div_lt_upper_bound; try order'. now rewrite <- pow_succ_r. * apply div_pos; order'. * rewrite <- (pow_1_r 2), <- 2 shiftr_div_pow2 by order'. rewrite <- shiftr_ldiff, H, shiftr_div_pow2, pow_1_r, div_0_l; order'. + rewrite <- 2 bit0_mod. apply bits_inj_iff in H. specialize (H 0). rewrite ldiff_spec, bits_0 in H. destruct a.[0], b.[0]; try discriminate; simpl; order'. } intros a b Hb Hd. assert (Ha : 0<=a). { apply le_ngt; intros Ha'. apply (lt_irrefl 0). rewrite <- Hd at 1. apply ldiff_neg. now split. } split; trivial. apply (AUX a); try split; trivial. apply pow_gt_lin_r; order'. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog