proposition: Lemma sub_nocarry_ldiff : forall a b, ldiff b a == 0 -> a-b == ldiff a b.
proof: Proof. intros a b H. apply add_cancel_r with b. rewrite sub_add. - symmetry. rewrite add_nocarry_lxor. + bitwise as m. apply bits_inj_iff in H. specialize (H m). rewrite ldiff_spec, bits_0 in H. now destruct a.[m], b.[m]. + apply land_ldiff. - now apply ldiff_le. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog