1. Write a function of type ∀ n m : nat, {n ≤ m} + {n > m}. That is, this function decides whether one natural is less than another, and its dependent type guarantees that its results are accurate.

2.(a) Define var, a type of propositional variables, as a synonym for nat.
(b) Define an inductive type prop of propositional logic formulas, consisting of variables, negation, and binary conjunction and disjunction.
(c) Define a function propDenote from variable truth assignments and props to Prop, based on the usual meanings of the connectives. Represent truth assignments as functions from var to bool.
(d) Define a function bool true dec that checks whether a boolean is true, with a maximally expressive dependent type. That is, the function should have type
    ∀ b, {b = true} + {b = true → False}.
(e) Define a function decide that determines whether a particular prop is true under a particular truth assignment. That is, the function should have type
    ∀ (truth : var → bool) (p : prop), {propDenote truth p} + { ̃ propDenote truth p}.
This function is probably easiest to write in the usual tactical style, instead of programming with refine. The function bool true dec may come in handy as a hint.
(f) Define a function negate that returns a simplified version of the negation of a prop. That is, the function should have type
    ∀ p : prop, {p’ : prop | ∀ truth, propDenote truth p ↔ ¬ propDenote truth p’ }
To simplify a variable, just negate it. Simplify a negation by returning its argument. Simplify conjunctions and disjunctions using De Morgan’s laws, negating the arguments recursively and switching the kind of connective. Your decide function may be useful in some of the proof obligations, even if you do not use it in the computational part of negate’s definition. Lemmas like decide allow us to compensate for the lack of a general Law of the Excluded Middle in CIC.