proposition: Lemma kth_S_sym : forall k n, kth_S k n = kth_S n k.
proof: Proof. induction k. intro. rewrite kth_S_special. reflexivity. intro. unfold kth_S. fold kth_S. rewrite IHk. induction n. compute. reflexivity. unfold kth_S. fold kth_S. rewrite IHn. reflexivity. Qed.
imports: PeanoNat Compare