proposition: Lemma product_incr_similarity : forall i m1 m1' m2 m2', itree_similar_upto i m1 m1' -> itree_similar_upto i m2 m2' -> itree_similar_upto (S i) (product m1 m2) (product m1' m2').
proof: Proof. Proof using. induction i using peano_induction. change (itree_similar_upto) with (family_sim itree_family). introv K1 K2. eapply cofe_similar_modulo. apply itree_family_COFE. rewrite <- itree_similar_eq. apply product_fixpoint. rewrite <- itree_similar_eq. apply product_fixpoint. simpl in K1, K2 |- *. destruct m1; destruct m2; simpl; auto. destruct m1'; destruct m2'; simple~. destruct~ i. inversions K1. destruct m1'; destruct m2'; simple~. destruct~ i. inversions K1. destruct m1'; destruct m2'; simple~. destruct~ i. inversions K2. destruct m1'; destruct m2'; simple~; destruct~ i. inversions K1. inversions K1. inversions K2. simpl in K1, K2. destruct K1. destruct K2. auto with maths. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat