931 apply (transfer, erule (1) mult_strict_left_mono) |
931 apply (transfer, erule (1) mult_strict_left_mono) |
932 apply (transfer, erule (1) mult_strict_right_mono) |
932 apply (transfer, erule (1) mult_strict_right_mono) |
933 done |
933 done |
934 |
934 |
935 instance star :: (pordered_comm_semiring) pordered_comm_semiring |
935 instance star :: (pordered_comm_semiring) pordered_comm_semiring |
936 by (intro_classes, transfer, rule mult_mono1_class.times_zero_less_eq_less.mult_mono1) |
936 by (intro_classes, transfer, rule mult_mono1_class.less_eq_less_times_zero.mult_mono1) |
937 |
937 |
938 instance star :: (pordered_cancel_comm_semiring) pordered_cancel_comm_semiring .. |
938 instance star :: (pordered_cancel_comm_semiring) pordered_cancel_comm_semiring .. |
939 |
939 |
940 instance star :: (ordered_comm_semiring_strict) ordered_comm_semiring_strict |
940 instance star :: (ordered_comm_semiring_strict) ordered_comm_semiring_strict |
941 by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.plus_times_zero_less_eq_less.mult_strict_mono) |
941 by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.plus_less_eq_less_zero_times.mult_strict_mono) |
942 |
942 |
943 instance star :: (pordered_ring) pordered_ring .. |
943 instance star :: (pordered_ring) pordered_ring .. |
944 instance star :: (pordered_ring_abs) pordered_ring_abs |
944 instance star :: (pordered_ring_abs) pordered_ring_abs |
945 by intro_classes (transfer, rule abs_eq_mult) |
945 by intro_classes (transfer, rule abs_eq_mult) |
946 instance star :: (lordered_ring) lordered_ring .. |
946 instance star :: (lordered_ring) lordered_ring .. |