proposition: Lemma scale_leq_ev : forall u v x : E, is_scale u -> is_scale v -> source u = source v -> target u = target v -> inc x (U (source u)) -> leq (target v) (ev u x) (ev v x).
proof: Proof. intros. unfold is_scale in H, H0; ee. apply (wo_induction H9 (p:=fun w : E => leq (target v) (ev u w) (ev v w))). intros. unfold is_well_ordered in H10; ee. unfold is_linear in H10; ee. apply linear_not_lt_leq. unfold is_well_ordered in H7; xe. unfold mor_axioms in H0; ee. unfold strong_axioms in H17; ee; unfold Umorphism.axioms in H17. apply H17. rewrite <- H1; am. rewrite <- H2. unfold mor_axioms in H; ee. unfold strong_axioms in H17; ee. ap H17; exact H12. intros. unfold lt in H16; ee. rewrite <- H2 in H16. pose (H11 _ _ H12 H16). induction e. ee. assert (lt (source u) x1 x0). apply scale_lt_back. unfold is_scale in |- *; ee. am. exact H5. exact H9. rewrite H2; am. am. am. am. rewrite H19. unfold lt in |- *; xe. assert (lt (target v) (ev v x1) (ev v x0)). apply injective_lt_lt. am. am. rewrite <- H1; am. assert (leq (target v) (ev u x1) (ev v x1)). apply H13. am. am. unfold lt in H21; ee. apply H23. apply leq_leq_eq with (target v). wr H2. am. exact H21. wr H19. exact H22. exact H3. Qed.
imports: universe