proposition: Lemma lor_eq_0_iff : forall a b, lor a b == 0 <-> a == 0 /\ b == 0.
proof: Proof. intros a b. split. - intro H; split. + now apply lor_eq_0_l in H. + rewrite lor_comm in H. now apply lor_eq_0_l in H. - intros (EQ,EQ'). now rewrite EQ, lor_0_l. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog