proposition: Lemma OT_sum_distributive3 a b c: order_type a -> order_type b -> order_type c -> c *t (a +t b) = (c *t a) +t (c *t b).
proof: Proof. move => oa ob oc. rewrite /OT_sum2 /OT_prod2; apply: order_type_unique. 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. have pa: order (order_prod2 (order_type_of c) (order_type_of a)). by apply: orprod2_or. have pb: order (order_prod2 (order_type_of c) (order_type_of b)). by apply: orprod2_or. have pc: order (order_sum2 (order_type_of a) (order_type_of b)). by apply: orsum2_or. rewrite OT_prop4 // OT_prop4 // OT_prop4 //. apply: (@orderIT (order_prod2 (order_type_of c) (order_sum2 (order_type_of a) (order_type_of b)))). apply: orprod_invariant4; [ by apply: orderIR | by apply: OT_prop0]. apply: (@orderIT (order_sum2 (order_prod2 (order_type_of c) (order_type_of a)) (order_prod2 (order_type_of c) (order_type_of b)))). apply: osum_distributive => //. by apply: orsum_invariant4;apply: order_type_exists. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)