proposition: Lemma ldiff_le : forall a b, ldiff a b == 0 -> a <= b.
proof: Proof. cut (forall n a b, a < 2^n -> ldiff a b == 0 -> a <= b). { intros H a b. apply (H a), pow_gt_lin_r; order'. } intro n; induct n. - intros a b Ha _. rewrite pow_0_r, one_succ, lt_succ_r in Ha. assert (Ha' : a == 0) by (generalize (le_0_l a); order'). rewrite Ha'. apply le_0_l. - intros n IH a b Ha 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_l. apply IH. * apply div_lt_upper_bound; trivial. now rewrite <- pow_succ_r'. * rewrite <- (pow_1_r 2), <- 2 shiftr_div_pow2. now rewrite <- shiftr_ldiff, H, shiftr_div_pow2, pow_1_r, div_0_l. + 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'. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog