proposition: Lemma le_canonical n m : {n <= m} + {~n <= m}.
proof: Proof. revert n; induction m; intro n. { destruct n. { left; constructor. } { right; clear. abstract auto with arith. } } { destruct (IHm n) as [IHm'|IHm']. { left; constructor; assumption. } { clear IHm'. specialize (IHm (pred n)). destruct IHm as [IHm|IHm], n; simpl in *. { left; constructor; assumption. } { left; apply le_SS; assumption. } { exfalso. abstract auto with arith. } { right; intro H. abstract (apply le_pred in H; simpl in *; auto). } } } Defined.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Classes.Morphisms Coq.Program.Basics