proposition: Lemma demo_lets_of : forall (x y : nat) (A B : Prop), (x > 0) -> (x <> y) -> (A <-> B) -> (forall n, n > 0 -> forall m, n <> m -> exists k, k <> m) -> (forall n : nat, n > 0 -> forall P Q : Prop, (P <-> Q) -> forall m : nat, n <> m -> forall K : nat -> Prop, K n -> forall p, K (m+p) -> True) -> True.
proof: Proof. Proof using. introv Pos Neq Iff L M. lets P: M Iff. eauto. clear P. lets P: (>> M Neq). eauto. eauto. clear P. lets P: (>> M __ y). eauto. eauto. clear P. lets P: (>> M x __ B). eauto. instantiate (1:=A) in P. clear P. lets P: (>> M __ y Neq). eauto. eauto. clear P. lets P: M Pos A B Neq. eauto. clear P. lets k K: (>> L Pos ___). eauto. clears k. lets k K: (>> L ___). eauto. eauto. clears k. forwards R: L. eauto. eauto. clear R. forwards R: L Pos. eauto. clear R. forwards k K: L. eauto. eauto. clears k. forwards [k K]: L Pos y. eauto. clears k. forwards k K: (>> L x y). eauto. eauto. clears k. lets k K: (>> L Neq). eauto. clears k. auto. Qed.
imports: TLC(LibTactics) Coq.micromega.Lia