le : nat → nat → Prop lt : nat → nat → Prop le : nat → nat → Prop lt : nat → nat → Prop le : nat → nat → Prop lt : nat → nat → Prop le : nat → nat → Prop lt : nat → nat → Prop