-rw-r--r-- 560 leangoppa-20230726/Goppadecoding/logic.lean raw
import Mathlib.Tactic

namespace Goppadecoding

section lemmas_logic

theorem not_eq_iff : a ≠ b ↔ ¬a = b := Iff.rfl

theorem and_imp_left {a b: Prop}: a ∧ b → a := by intro a_1; simp_all only

theorem and_imp_right {a b: Prop}: a ∧ b → b := by intro a_1; simp_all only

theorem ite_le_ite (P : Prop) [Decidable P] {O: Type _} [Preorder O] {a b c d: O}:
  a ≤ c → b ≤ d → ((if P then a else b) ≤ (if P then c else d)) :=
by
  intro ac bd
  by_cases h: P
  . simp only [h, ite_true, ac]
  . simp only [h, ite_false, bd]

end lemmas_logic