proposition: Lemma demo_invert : even_shift 4 8 -> False.
proof: Proof. Proof using. intros P. dup 12. inversion P. inversion H7. inversion H10. inversions P. inversions H7. inversions H8. invert P. introv P' EQ1 EQ2. demo. invert P as P' EQ1 EQ2. demo. inverts P. inverts H7. inverts H8. inverts P as P'. inverts P' as P''. inverts P''. inverts P as P. inverts P as P. inverts P. inverts P as. introv P'. demo. invert keep P. intros. demo. inverts keep P as P' EQ1 EQ2. demo. inverts keep P as. introv P'. demo. lets_inverts (conj P P) as H1 H2. demo. Qed.
imports: TLC(LibTactics) Coq.micromega.Lia