Theorem le_trans: forall n m o, n <= m -> m <= o -> n <= o.
Proof.
intros n m o Lnm Lmo.
generalize dependent Lnm.
generalize dependent n.
induction Lmo.
-intros. apply Lnm.
-intros. apply le_S. apply IHLmo. apply Lnm.
Qed.
how to prove :
Theorem le_antisym: forall n m, n <= m -> m <= n -> n = m.
I don’t know if there is a relationship between the two propositions, if I need to use the first proposition to aid in proving the second, and if so, how to prove it, and if not, how to prove it
New contributor
sesame ball is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.