proposition: Lemma le_Sn_n n : S n <= n -> False.
proof: Proof. intros. apply le_subterm in H as [Heq|Hlt]. depelim Heq. apply well_founded_antisym in Hlt. auto. repeat constructor. Qed.
imports: Program Equations.Prop.EqDecInstances Equations.Prop.Equations