proposition: Lemma demo_sort : forall n : nat, n > 0 -> forall P Q : Prop, (P <-> Q) -> forall m : nat, m <> n -> forall K : nat -> Prop, K n -> forall p, K (m+p) -> True.
proof: Proof. Proof using. intros. sort. demo. Qed.
imports: TLC(LibTactics) Coq.micromega.Lia