[intros;simplify;rewrite < plus_n_Sm in H2;simplify in H2;
rewrite < plus_n_O in H2;rewrite < minus_n_O in H2;
rewrite > (antisymmetric_le k n H1 H2);apply in_list_head
[intros;simplify;rewrite < plus_n_Sm in H2;simplify in H2;
rewrite < plus_n_O in H2;rewrite < minus_n_O in H2;
rewrite > (antisymmetric_le k n H1 H2);apply in_list_head