You can answer either one or both

You can answer either one or both.

-- a. Only one of the following two theorems is provable. Figure out
-- which one is true, and replace the sorry command with a complete
-- proof in lean.
section
 parameters {A : Type} {a b c : A} {R : A → A → Prop}
 parameter (Rab : R a b)
 parameter (Rbc : R b c)
 parameter (nRac : ¬ R a c)

 theorem R_is_strict_partial_order : irreflexive R ∧ transitive R :=
 sorry

 theorem R_is_not_strict_partial_order : ¬(irreflexive R ∧ transitive R) :=
 sorry
end

-- b, separate question
section
 open nat

 example : 1 ≤ 4 :=
 sorry
end