// We just looked at these three rules to encode the meaning of "and".

lemma ProveAnd(P: bool, Q: bool)
  requires P
  requires Q
  ensures P && Q
{
}

lemma UseAnd1(P: bool, Q: bool)
  requires P && Q
  ensures P
{
}

lemma UseAnd2(P: bool, Q: bool)
  requires P && Q
  ensures Q
{
}

// YOUR CHALLENGE: look for three lemmas that similarly capture the full meaning of "or".
// That is, anything we can prove about uses of "or" should follow from just your lemmas,
// if we then go and forget the inherent meaning of "or".
// Hint: there is a nice symmetry between "and" and "or", but it's not quite trivial.
// You will probably want two "Prove" rules and one "Use" rule (flipping the situation for "and").
// You will probably also want to use some other logical connective beside just "or".