proposition: Lemma lor_nonneg : forall a b, 0 <= lor a b <-> 0<=a /\ 0<=b.
proof: Proof. intros a b. rewrite 3 bits_iff_nonneg_ex. split. - intros (k,Hk). split; exists k; intros m Hm; apply (orb_false_elim a.[m] b.[m]); rewrite <- lor_spec; now apply Hk. - intros ((k,Hk),(k',Hk')). destruct (le_ge_cases k k'); [ exists k' | exists k ]; intros m Hm; rewrite lor_spec, Hk, Hk'; trivial; order. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog