proposition: Lemma lxor_nonneg : forall a b, 0 <= lxor a b <-> (0<=a <-> 0<=b).
proof: Proof. assert (H : forall a b, 0<=a -> 0<=b -> 0<=lxor a b). { intros a b. rewrite 3 bits_iff_nonneg_ex. intros (k,Hk) (k', Hk'). destruct (le_ge_cases k k'); [ exists k' | exists k]; intros m Hm; rewrite lxor_spec, Hk, Hk'; trivial; order. } assert (H' : forall a b, 0<=a -> b<0 -> lxor a b<0). { intros a b. rewrite bits_iff_nonneg_ex, 2 bits_iff_neg_ex. intros (k,Hk) (k', Hk'). destruct (le_ge_cases k k'); [ exists k' | exists k]; intros m Hm; rewrite lxor_spec, Hk, Hk'; trivial; order. } intros a b. split. - intros Hab. split. + intros Ha. destruct (le_gt_cases 0 b) as [Hb|Hb]; trivial. generalize (H' _ _ Ha Hb). order. + intros Hb. destruct (le_gt_cases 0 a) as [Ha|Ha]; trivial. generalize (H' _ _ Hb Ha). rewrite lxor_comm. order. - intros E. destruct (le_gt_cases 0 a) as [Ha|Ha]. + apply H; trivial. apply E; trivial. + destruct (le_gt_cases 0 b) as [Hb|Hb]. * apply H; trivial. apply E; trivial. * rewrite <- lxor_lnot_lnot. apply H; now apply lnot_nonneg. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog