proposition: Theorem le_reverse_rules : forall n m:nat, n <= m -> n = m \/ exists p, n <= p /\ m = S p.
proof: Proof. intros n m H; inversion_clear H. left;trivial. right; exists m0; split; trivial. Qed.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List