proposition: Lemma next_leq_gen_leq : forall a x y, is_well_ordered a -> inc x (U a) -> inc y (U a) -> leq_gen (next a) x y = leq a x y.
proof: Proof. ir. ap leq_gen_leq. ap next_compatible_next; am. am. am. Qed.
imports: Arith order