proposition: Lemma OT_sum_assoc3 a b c: order_type a -> order_type b -> order_type c -> a +t (b +t c) = (a +t b) +t c.
proof: Proof. move => oa ob oc. have xoa: order (order_type_of a) by apply: OT_prop3; apply: OT_prop2. have xob: order (order_type_of b) by apply: OT_prop3; apply: OT_prop2. have xoc: order (order_type_of c) by apply: OT_prop3; apply: OT_prop2. rewrite/OT_sum2; apply: order_type_unique. have pa: order (order_sum2 (order_type_of b) (order_type_of c)). by apply: orsum2_or. have pb: order (order_sum2 (order_type_of a) (order_type_of b)). by apply: orsum2_or. rewrite OT_prop4 // OT_prop4 //. apply: (@orderIT (order_sum2 (order_type_of a) (order_sum2 (order_type_of b) (order_type_of c)))). apply: orsum_invariant4; [by apply: orderIR | by apply: OT_prop0 ]. apply: (@orderIT (order_sum2 (order_sum2 (order_type_of a) (order_type_of b))(order_type_of c))). apply: osum_assoc2; fprops. apply: orsum_invariant4; [ by apply: order_type_exists | by apply: orderIR]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)