proposition: Lemma demo_applys_specializes : forall (x y : nat) (A B : Prop), (x > 0) -> (x <> y) -> (A <-> B) -> (forall n : nat, n > 0 -> forall P Q : Prop, (P <-> Q) -> forall m : nat, m <> n -> True) -> True.
proof: Proof. Proof using. introv Pos Neq Iff M. dup 17. applys (>> M Pos). eauto. eauto. applys (>> M A B). eauto. eauto. eauto. applys (>> M Pos Iff). eauto. applys (>> M Iff). eauto. eauto. applys (>> M x Iff). eauto. eauto. applys M x Iff. eauto. eauto. specializes M (>> 3). auto. specializes M (>> 3 A B). auto. auto. specializes M (>> A __ __). eauto. eauto. auto. specializes M (>> Pos Iff 2). eauto. auto. specializes M (>> Pos ___). eauto. eauto. auto. specializes M (>> __ B ___). eauto. eauto. eauto. auto. specializes M __. specializes M __. eauto. auto. specializes M ___. eauto. eauto. eauto. auto. applys (>> M (rm Pos) Iff). eauto. specializes M (>> (proj1 (conj (rm Pos) Neq))). auto. Qed.
imports: TLC(LibTactics) Coq.micromega.Lia