Commit 2022-07-17 06:40 e42057fa

feat(data/nat/bitwise): tweak lxor lemmas (#15409) This PR does the following:

• add lxor_cancel_right, lxor_cancel_left, lt_lxor_cases.
• make lxor_right_inj and lxor_left_inj into iffs as per convention, prove the corresponding lxor_right_injective and lxor_left_injective separately.
• golf lxor_eq_zero, tag it as simp, add the corresponding lxor_ne_zero lemma.
• simplify the hypothesis of lxor_trichotomy.