proposition: Lemma dot_product_mon_r : forall i j (jp : (j < i)%nat) (v v' w w' : vector nat i), v >=v v' -> w >=v w' -> Vnth v jp > A0 -> Vnth w jp > Vnth w' jp -> dot_product v w > dot_product v' w'.
proof: Proof. intros i j. gen i. clear i. induction j; intros. destruct i. lia. VSntac v. VSntac w. VSntac v'. VSntac w'. unfold dot_product. simpl. fold (dot_product (Vtail v') (Vtail w')). fold (dot_product (Vtail v) (Vtail w)). unfold Aplus, Peano.gt. apply plus_gt_compat_r. apply dot_product_mon; apply Vforall2_tail; hyp. rewrite !Vhead_nth. apply mult_lt_compat_lr. apply (Vforall2_elim_nth (R:=ge)). hyp. rewrite (lt_unique (Nat.lt_0_succ i) jp). hyp. rewrite (lt_unique (Nat.lt_0_succ i) jp). hyp. destruct i. lia. VSntac v. VSntac w. VSntac v'. VSntac w'. unfold dot_product. simpl. fold (dot_product (Vtail v') (Vtail w')). fold (dot_product (Vtail v) (Vtail w)). unfold Aplus, Peano.gt. apply plus_gt_compat_l. apply IHj with (NatCompat.lt_S_n jp). apply Vforall2_tail. hyp. apply Vforall2_tail. hyp. rewrite Vnth_tail, lt_nS_Sn. hyp. rewrite !Vnth_tail, lt_nS_Sn. hyp. apply Nat.mul_le_mono. rewrite !Vhead_nth. apply (Vforall2_elim_nth (R:=ge)). hyp. rewrite !Vhead_nth. apply (Vforall2_elim_nth (R:=ge)). hyp. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil AWFMInterpretation NatUtil AMatrixBasedInt)