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; trivial. - 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. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog