Some simple proofs

Please copy the file SRC/simple_proofs and replace the automatic proof tactic auto with the elementary tactics assumption, intros, and apply.