proposition: Theorem exists_example_2 : forall n, (exists m, n = 4 + m) -> (exists o, n = 2 + o).
proof: Proof. MProof. cintros n {- destructn 0 &> intros m Hm -}. simpl. mexists (2 + m). apply Hm. Qed.
imports: Mtac2.Mtac2 Lists.List