proposition: Lemma nocarry_equiv : forall a b c, c/2 == lnextcarry a b c -> c.[0] = false -> (c == 0 <-> land a b == 0).
proof: Proof. intros a b c H H'. split. - intros EQ; rewrite EQ in *. rewrite div_0_l in H by order'. symmetry in H. now apply lor_eq_0_l in H. - intros EQ. rewrite EQ, lor_0_l in H. apply bits_inj'. intros n Hn. rewrite bits_0. apply le_ind with (4:=Hn). + solve_proper. + trivial. + clear n Hn. intros n Hn IH. rewrite <- div2_bits, H; trivial. autorewrite with bitwise. now rewrite IH. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog