fact: Fixpoint left_edge_aux {A B : Type}n (m : triangular A B n): B * t A n:= match m with base b => (b,@nil A ) | @line _ _ p b t' => match left_edge_aux p t' with (x,y,l) => (b,(cons A x _ l)) end end.
imports: Vector